elias001
- 389
- 30
@fresh_42 it might be more than just a nice project. Imagine in the near future, anyone want fmto submit articles to a math journal is required to first formalise any theorems in their paper in Lean, and see if it passes muster according to Lean, then submit the article along with the Lean code. You aer going to tell professors who are teaching their students on how to do proofs using Lean that they should not be teaching their students to rely on it? Like I said, you should speak to the CS people on the Formal Verification of software and ask their opinions on the matter. It might or will be a matter of time before there are add on packages for proof checking into Maple mathematica and Matlab.