5 ms·
It would be nice if we had a mathematics-wide push for formal verification of proofs, not just done by the mathematicians who really like formal verification. M
by etaioinshrdlu 5y ago
It would be nice if we had a mathematics-wide push for formal verification of proofs, not just done by the mathematicians who really like formal verification. Maybe there could be a journal of only formally-verfified results?
- Someone 5y agohttps://sciendo.com/journal/FORMA https://sciendo.com/journal/FORMA gets close, I think (I don’t think it only publishes formally verified results. It likely also accepts more philosophical texts about formal verification). There’s also http://mizar.org/JFM/ http://mizar.org/JFM/ I don’t think such journals can be the full solution, though. Problem is that to entice mathematicians who don’t like formal verification to publish in it.
- z77dj3kl 5y agoWhat do you mean? Mathematics is all about formal verification, i.e. proofs.
- SAI_Peregrinus 5y agoI think they mean computer-verified proofs. As you note, the existing proofs are already formally verified, so this might not add much.
- jkhdigital 5y agoHomotopy type theory is just that: https://www.ias.edu/ideas/2014/voevodsky-origins https://www.ias.edu/ideas/2014/voevodsky-origins
- deadbeef57 5y agoHomotopy type theory (HoTT) can mean several things: it's a new foundation of mathematics that was developed from the start with computer-formalization in mind. But you can also work on HoTT without ever touching a computer. Conversely, there are many ways to do computer-formalization of mathematics, without every doing anything with HoTT.