Timeline for At which level is it currently possible to write formal proofs?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 28, 2022 at 9:09 | history | edited | Martin Sleziak | CC BY-SA 4.0 |
http -> https (the question was bumped anyway)
|
| Jun 22, 2013 at 18:04 | comment | added | The User | Well, that was not what I was looking for (the answer would have probably been “very low-level, except of some cases”), but it gives an interesting perspective, telling that some “high-level” mathematics are possible, circumvening some restrictions. Thanks a lot! | |
| Jun 22, 2013 at 18:01 | vote | accept | The User | ||
| Jun 18, 2013 at 19:12 | comment | added | Urs Schreiber | That's it, yes. Go for it. | |
| Jun 18, 2013 at 18:08 | comment | added | The User | Uh, isn’t it just github.com/HoTT/book ? Using latexmk with the correct parameters it looks just like a book about HoTT called HoTT Univalent Foundations of Mathematics. | |
| Jun 18, 2013 at 17:49 | comment | added | Urs Schreiber | That book would seem to be the single best place to start for people in need of an introduction to the topic, yes. The only problem is that it is, while pretty much done, not quite published yet. A preliminary copy has been circulating in the IAS mailing list, though. If you want to look at it I think you can email one of the usual suspects and ask for the preliminary version. | |
| Jun 18, 2013 at 16:26 | comment | added | The User | Can you recommend the HoTT Univalent Foundations of Mathematics book? It looks quite elementary, or does it require any specialised knowledge, which I did not notice? | |
| Jun 18, 2013 at 8:00 | history | answered | Urs Schreiber | CC BY-SA 3.0 |