LLMs are making formal software verification feasible at a much larger scale
16
votes
Showing only topics with the tag "proofs".
Back to normal view
-
-
Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
25 votes -
Overview of the proofs behind the Navier-Stokes $1 million millennium prize problem
29 votes -
The four-color theorem gets a rare new proof
14 votes -
Postmortem for Lean kernel soundness bug #14576
12 votes -
Human mathematicians are being outcounterexampled
37 votes -
How Terry Tao became an evangelist for AI in math
12 votes -
An OpenAI model has disproven a central conjecture in discrete geometry
35 votes -
Introducing Gauss, an agent for autoformalization
7 votes -
Kneading dough is chaotic
3 votes -
Formalizing Fermat’s Last Theorem - How it’s going
4 votes -
AI will become mathematicians’ ‘co-pilot’
5 votes -
Division by zero in type theory: a FAQ
4 votes