Timeline for What is the endgoal of formalising mathematics?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 16 at 9:02 | comment | added | C7X | About #1 and #4, Naproche (natural language proof checker, page naproche.github.io) is a proof checker with a syntax that resembles natural proof, which to my knowledge uses an automated theorem prover to fill in the usual kind of smaller steps left implicit in the proof. | |
| Feb 8, 2021 at 11:15 | comment | added | Blaisorblade | Re 5., proof assistants will happily accept axioms; formalizing definitions might still be nontrivial, but e.g. Buzzard argues it can be “fast enough” (he formalized perfectoid spaces after all). You “just” need the axioms you state to be “true enough” as written and to disambiguate the on-paper notation correctly. | |
| Dec 10, 2020 at 8:48 | comment | added | Jordan Barrett | Kevin Buzzard gives a similar list (and his opinion is probably more informed than mine) from 11 mins onwards in youtube.com/watch?v=q5-pykbfViA | |
| Dec 10, 2020 at 7:48 | comment | added | Manuel Eberl | I don't think being based on set theory has anything to do with what input syntax provers offer. Isabelle also has declarative proof syntax, which is probably still quite a bit away from what you are looking for, but certainly closer than most systems. (see the examples here). | |
| Dec 10, 2020 at 3:33 | comment | added | Daniel R. Collins | Historical minutiae: When the BASIC programming language first appeared in 1964, defining a new object (variable) did in fact require the keyword "LET", for precisely the math-idiom reasons seen here. But over time that was considered burdensome, and the use of LET was made optional and then dropped (instead, the first time a new variable is seen it's assumed to be declared). dartmouth.edu/basicfifty/commands.html | |
| Dec 10, 2020 at 0:25 | history | made wiki | Post Made Community Wiki by Todd Trimble | ||
| Dec 9, 2020 at 23:35 | comment | added | Timothy Chow | In terms of proofs that look more like natural language, the proof assistants based on set theory tend to be more readable; see the Mizar examples in Freek Wiedijk's Notices article. Also, set-theoretic proof assistants arguably are closer to mathematicians' intuition. I discuss some of the objections to set-theoretic proof assistants in another MO answer. | |
| Dec 9, 2020 at 22:55 | comment | added | Wojowu | Overall though, I do agree with the sentiment that there is some work left to be done to make proof assitants more mathematician-friendly. Kevin Buzzard is very vocal in expressing his frustration when first learning Lean and how the documentation was written "by computer scientists for computer scientists". One has to remember though that someone has to build those programs, and someone with nearly enough programming proficiency to more than likely to come from CS background than math one. | |
| Dec 9, 2020 at 22:51 | comment | added | Wojowu | As an absolute non-expert, let me make some comments. 1. Natural language is ambiguous. Any attempt to make it unambiguous is bound to make the language more "mechanical". Sure some basic things like "let" can be simplified, but quickly it will be less feasible. 4. You are asking for (what in Lean at least is called) tactics. Many such exist, for instance there is one which will automatically prove any identity in the language of commutative rings. 5. This is already (to an extent) happening. However, the entry barrier is high, so almost everyone is first working out the basics.. | |
| Dec 9, 2020 at 21:48 | history | answered | Jordan Barrett | CC BY-SA 4.0 |