LEAN The New Way to Prove Theorems

  • Context: High School 
  • Thread starter Thread starter jedishrfu
  • Start date Start date
Click For Summary

Discussion Overview

The discussion revolves around the use of the LEAN theorem prover in mathematical research, particularly its potential and limitations in proving theorems. Participants explore its current capabilities, the historical context of similar tools, and the implications for future mathematical work.

Discussion Character

  • Exploratory
  • Debate/contested
  • Technical explanation

Main Points Raised

  • Some participants share resources related to LEAN programming, indicating a growing interest in its application.
  • A participant cites Heather Macbeth's perspective that LEAN may take decades to become a reliable research tool, contrasting it with the more established Coq system.
  • Concerns are raised about the limitations of LEAN's current mathematical library, particularly its lack of support for complex analysis and differential equations.
  • One participant questions whether using LEAN will require redoing substantial work already done in Coq, highlighting potential redundancy in efforts.
  • Another participant expresses skepticism about the impact of theorem provers on the types of mathematical problems that researchers may pursue, suggesting that reliance on these systems could shape research directions.

Areas of Agreement / Disagreement

Participants express a mix of interest and skepticism regarding LEAN's capabilities and future role in mathematics. There is no consensus on its effectiveness or the implications of its use in research.

Contextual Notes

Limitations include the current scope of LEAN's mathematical library and the historical context of theorem provers like Coq, which may affect the perceived utility of LEAN.

Mathematics news on Phys.org
“It will likely be decades before [Lean] is a research tool,” said Heather Macbeth of Fordham University, a fellow Lean user.
“Coq is an old man now, and it has a lot of scars,” said Mahboubi, who has worked with the program extensively. “It’s been collaboratively maintained by many people over time, and it has known defects due to its long history.”
What could possibly go wrong?
 
  • Informative
Likes   Reactions: S.G. Janssens
The best laid plans of mathematicians and men.
 
Thank you for this. I tend to be sceptical about theorem provers, specially in analysis:
These are the ingredients that mathematicians can mix together in Lean to make mathematics. Right now, despite those numbers, it’s a limited pantry. It contains almost nothing from complex analysis or differential equations — two basic elements of many fields of higher math
However, its interesting and good to keep an eye on. Two concerns:
  1. Does this involve redoing a substantial amount of the work that already served as input for Coq?
  2. If people start to depend on these systems for actual research, then to what extend is the computer's aptness for certain kinds of mathematics going to dictate what sort of problems people will work on?
 

Similar threads

High School New solutions to old, historic problems
  • · Replies 2 ·
Replies
2
Views
3K
Undergrad Isn't it terrifying that AI can become smarter than any Mathematician?
  • · Replies 40 ·
2
Replies
40
Views
6K
High School Retired Statistician Proves GCI Theorem
  • · Replies 1 ·
Replies
1
Views
1K
High School Three Squares Problem
  • · Replies 10 ·
Replies
10
Views
2K
High School Understanding the Pythagorean Theorem
  • · Replies 38 ·
2
Replies
38
Views
6K
High School Is this a new theorem?
  • · Replies 9 ·
Replies
9
Views
2K
High School Have I proved some part of Fermat's last theorem?
  • · Replies 15 ·
Replies
15
Views
3K
High School Are there English names for these formulas? (binomial formulas)
  • · Replies 42 ·
2
Replies
42
Views
6K
Insights Fermat's Last Theorem
  • · Replies 105 ·
4
Replies
105
Views
10K
High School A triangle problem: Prove that |AC|+|AB|=|PR|+|PQ| given some constraints
  • · Replies 13 ·
Replies
13
Views
3K