3 ms·
Sorry for the dim question, but could you explain what is wrong with Lean's method? I was wondering this when looking at the slides, too. (We know 2 != 1, there
by lordgrenville 7y ago
Sorry for the dim question, but could you explain what is wrong with Lean's method? I was wondering this when looking at the slides, too. (We know 2 != 1, therefore False - right?)
- krapht 7y agoThe point is asking the user to prove this is basically asking the user to write proof assembly language, not that it is incorrect.
- Someone 7y agoWe know, but Lean (initially) didn’t. When writing a computer theorem prover/checker, you want the part that isn’t proven by the system itself to be bug-free first, and expressive second. The only way to get the first is by giving up that second goal. So, you rather give your users something bug free in which they can express the basics of numbers, starting, for example, with the Peano axioms (https://en.wikipedia.org/wiki/Peano_axioms https://en.wikipedia.org/wiki/Peano_axioms) (and that isn’t even the bottom of the stack; an even more basic system could replicate Principia Mathematica (https://en.wikipedia.org/wiki/Principia_Mathematica) https://en.wikipedia.org/wiki/Principia_Mathematica)) It’s a long road from there to high school math and an even longer one to mathematics research, so users not only will be able to do the above, but they will have to, if they want to do something at the front of mathematics.