Timeline for What makes dependent type theory more suitable than set theory for proof assistants?
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 20, 2020 at 16:55 | comment | added | Mario Carneiro | ... The current proof assistant I am working in, Metamath Zero, is based on peano arithmetic, not even set theory, and a ring tactic would be similarly easy to write as in lean. This has more to do with the framework around the language rather than the formal system (in Andrej's terminology: $M$ matters for writing automation, not $F$), and the problem with Metamath is that $M$ is in no way encoded in the "deliverables", so every author must discover it for themselves. | |
| Nov 20, 2020 at 16:52 | comment | added | Mario Carneiro |
Part of the reason I didn't write ring for Metamath is because there weren't that many examples that came up that couldn't be done manually with a better proof; in metamath a tactic that creates ugly proofs is a much harder sell because every single line of the proof is laid bare for everyone to read. The numeric evaluator (aka norm_num in lean) was written in metamath and contains the same techniques as a ring tactic would have.
|
|
| Nov 20, 2020 at 14:28 | comment | added | Kevin Buzzard | So echoing a comment that Andrej made -- as well as asking "what can be done in theory?", in this game an equally important question is "what can be done in practice?" Mario Carneiro is an expert in both Metamath and Lean, and he wrote Lean's ring tactic in just a few days as far as I could see, but Metamath still has no ring tactic. | |
| Nov 20, 2020 at 14:10 | history | edited | Kevin Buzzard | CC BY-SA 4.0 |
clarification
|
| Nov 20, 2020 at 13:59 | history | answered | Kevin Buzzard | CC BY-SA 4.0 |