Hacker News new | past | comments | ask | show | jobs | submit
robinzfc | on: GPT-5.6 used a prompt to close a 30-year gap in convex optimization
Mizar is an early theorem prover. It still exists, see the 2025 issue of Formalized Mathematics journal [1] that publishes math articles formally verified by Mizar (since 1990).

[1] https://reference-global.com/issue/FORMA/33/1