High School LEAN The New Way to Prove Theorems

  • Thread starter Thread starter jedishrfu
  • Start date Start date
Click For Summary
LEAN is emerging as a promising tool for proving theorems, but it is still in its early stages, with experts predicting it will take decades to become a fully functional research tool. Current limitations include a lack of resources in key areas like complex analysis and differential equations, which are essential for advanced mathematics. Concerns have been raised about the potential need to redo significant work already accomplished in Coq, a more established theorem prover. Additionally, there is apprehension that reliance on systems like LEAN could influence the types of mathematical problems researchers choose to pursue. Overall, while LEAN shows potential, its development and integration into mathematical research will require careful consideration.
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 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?
 

Thread 'Area of Overlapping Squares'

Here is a little puzzle from the book 100 Geometric Games by Pierre Berloquin. The side of a small square is one meter long and the side of a larger square one and a half meters long. One vertex of the large square is at the center of the small square. The side of the large square cuts two sides of the small square into one- third parts and two-thirds parts. What is the area where the squares overlap?
View full post »

Similar threads

Undergrad Monumental Proof Settles Geometric Langlands Conjecture
  • · Replies 1 ·
Replies
1
Views
2K
Undergrad Isn't it terrifying that AI can become smarter than any Mathematician?
  • · Replies 40 ·
2
Replies
40
Views
6K
High School New solutions to old, historic problems
  • · Replies 2 ·
Replies
2
Views
2K
High School Retired Statistician Proves GCI Theorem
  • · Replies 1 ·
Replies
1
Views
1K
Undergrad The answer is 15! What is the problem?
  • · Replies 1 ·
Replies
1
Views
2K
High School A triangle problem: Prove that |AC|+|AB|=|PR|+|PQ| given some constraints
  • · Replies 13 ·
Replies
13
Views
3K
Insights Fermat's Last Theorem
  • · Replies 105 ·
4
Replies
105
Views
8K
Prove the 2nd axiom of mathematical logic using the Deduction Theorem
  • · Replies 1 ·
Replies
1
Views
2K
High School Have I proved some part of Fermat's last theorem?
  • · Replies 15 ·
Replies
15
Views
2K
MHB Can high school math prove this inequality?
  • · Replies 7 ·
Replies
7
Views
2K