Timeline for At which level is it currently possible to write formal proofs?
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 28, 2022 at 9:26 | answer | added | Gro-Tsen | timeline score: 9 | |
| Jun 22, 2013 at 18:01 | vote | accept | The User | ||
| Jun 18, 2013 at 8:00 | answer | added | Urs Schreiber | timeline score: 13 | |
| Jun 18, 2013 at 2:34 | answer | added | Jacques Carette | timeline score: 12 | |
| Jun 18, 2013 at 0:49 | history | edited | The User | CC BY-SA 3.0 |
there should not be a ,
|
| Jun 14, 2013 at 10:20 | history | edited | The User | CC BY-SA 3.0 |
added 138 characters in body; added 23 characters in body
|
| Jun 13, 2013 at 10:10 | comment | added | The User | I have already heard about it, but all examples they are referring to seem to be direct derivations of some basic theorems starting directly from some axioms. Current development seems to be more focused on proving (in an empirical sense) the feasibility of the usage of natural language in proof assistants, while there are already some formalised, more abstract theories for more established proof systems (but as an outsider I cannot judge their usability and their extents, that is the reason for my question). Correct me if I am wrong. | |
| Jun 13, 2013 at 9:00 | comment | added | Joel David Hamkins | You might be interested in the Naproche system---see mathoverflow.net/questions/55458/writing-semi-formal-proofs/…, and follow through. | |
| Jun 12, 2013 at 23:08 | history | asked | The User | CC BY-SA 3.0 |