Re:Some stuff I found interesting about number theory research
by etaioinshrdlu on Monday July 26, 2021 @02:13AM
(#27956237)
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?
[ Parent
| on HN ]
Re:Some stuff I found interesting about number theory research
by Someone on Monday July 26, 2021 @02:38AM
(#27956385)
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/
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.
Re:Some stuff I found interesting about number theory research
by jkhdigital on Monday July 26, 2021 @07:23AM
(#27958108)
Homotopy type theory is just that: https://www.ias.edu/ideas/2014/voevodsky-origins
Re:Some stuff I found interesting about number theory research
by deadbeef57 on Monday July 26, 2021 @01:46PM
(#27962552)
Homotopy 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.
Re:Some stuff I found interesting about number theory research
by z77dj3kl on Monday July 26, 2021 @06:55AM
(#27957943)
What do you mean? Mathematics is all about formal verification, i.e. proofs.
Re:Some stuff I found interesting about number theory research
by SAI_Peregrinus on Monday July 26, 2021 @01:10PM
(#27962029)
I think they mean computer-verified proofs. As you note, the existing proofs are already formally verified, so this might not add much.