Formal-Verification

TL;DR for operators When an AI system produces a formal proof, an evaluation team can make one part of the verdict unusually objective: either the proof is accepted under the allowed rules, or it is not. That removes much of the grader variance found in rubric scoring or LLM judging. AxQM provides 1,019 Lean 4 proof-synthesis tasks over 479 finite-dimensional quantum-mechanics textbook items. It keeps a private reference solution for every task and grades submissions through successful compilation, absence of sorry in the proof or its dependencies, and absence of newly introduced axioms.1 ...

TL;DR for operators A model can produce a correct answer while taking a logically invalid route to get there. That distinction matters whenever downstream execution depends not only on the answer, but on whether the intermediate decisions are trustworthy. Chen, Zhou, and Zhang test a lighter alternative to full theorem-proof generation: PRoSFI, which asks a 7B model to expose small, machine-readable reasoning steps that external formal tools can verify.1 On ProverQA-Hard, outcome-only reinforcement learning reaches 91.31% answer accuracy but only 21.97% GPT Soundness. PRoSFI reaches 92.97% accuracy and 76.07% GPT Soundness. The practical lesson is not that every business workflow should be formalized. It is that when intermediate decisions can be expressed as checkable rules, adding a verification layer can provide a stronger reliability signal than final-answer accuracy alone. ...

TL;DR for operators When software is intentionally allowed to disclose some sensitive information, a release rule and proof of compliance should not be the same object. David A. Naumann’s Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI1 repairs an earlier framework by giving permitted information release an explicit meaning, then separately defining whether an observer learned more than that policy allows. ...

TL;DR for operators The strongest result in this case study is not that an AI system wrote working Prolog. Across 33 targeted exercises, Claude generated 508 runtime tests alongside 257 lemmas and roughly 11,800 lines of proof, with the authors manually inspecting the generated files and an independent theorem prover checking the proofs. ...

TL;DR for operators A technically sophisticated AI answer is still only a candidate. Coherent explanations, detailed equations, and confident conclusions cannot substitute for an independent check of whether the reasoning is valid. Kol and colleagues report such a check for a layered quantum optimization method called QAOA. Lean 4’s kernel verifies that, for an even ring with $2p+2 \le n$, the optimal approximation ratio at depth $p$ is exactly ...

Failure should be boring Approval workflows are supposed to be boring. A client submits documents, a system checks the required conditions, and an approval either happens or does not happen. Boring is good. Boring means the process does not accidentally approve a case while also escalating it as problematic. The trouble begins when a workflow is written as a best-effort model of reality. Someone encodes the actions. Someone else adds an exception. A third person adds a shortcut because the quarterly dashboard prefers speed over philosophy. Eventually, a sequence exists that should not exist. It does not look like a bug when inspected locally. Each action seems defensible. The path as a whole is the problem. ...

Mathematics has a management problem. That sounds less romantic than saying it has a reasoning problem, but romance is not usually where bottlenecks hide. A proof can be brilliant, a referee can be diligent, and still the verification system can fail for the boring reason that nobody has enough time to check everything line by line. The paper Automatic Textbook Formalization takes that bottleneck seriously and then does something unusually concrete: it reports a multi-agent system that formalized a 500-plus-page graduate algebraic combinatorics textbook into Lean, with all 340 target definitions and theorems proved, in about one week.1 ...

When Less Proves More: The Case for Minimalist AI Theorem Provers Proof is a good place to test AI humility. In ordinary business writing, a model can sound confident, cite familiar patterns, and still be quietly wrong. The error may not surface until the contract is signed, the policy memo is circulated, or the spreadsheet has already acquired the authority of a sacred object. In formal theorem proving, the arrangement is less polite. The model writes code. Lean compiles it. The compiler either accepts the proof or sends it back covered in red ink. ...

Agents now do things. That sounds obvious, but it is the entire problem. A chatbot can be wrong and mostly embarrass itself. An agent can book the wrong hotel, leak the wrong file, fabricate the wrong report, or move through a workflow with the quiet confidence of a junior employee who has just discovered automation and has not yet discovered liability. ...

Compute is a very convenient alibi. When an AI system fails, the modern reflex is to ask for more of it: more samples, more tokens, more search, more GPUs, more patience from whoever is paying the invoice. This habit is not always wrong. Sometimes the model really does need another attempt. Sometimes the winning answer is hiding in sample number 47. ...