What Mathematical Conjecture Solving Means for Clinical AI Safety

The most useful thing about recent work in AI mathematical reasoning and conjecture solving is not that an AI system can now produce impressive mathematical artifacts. It is that some of those artifacts can be checked by a machine that does not care how persuasive the explanation sounds.

That distinction matters for clinical AI. A diagnostic model can look coherent, a code assistant can generate plausible device software, and a post-market monitoring plan can sound disciplined. None of that is the same as knowing that a defined behavior holds for every input covered by a specification. Formal verification tries to make that narrower claim: not that the system is generally safe, and not that clinical uncertainty has disappeared, but that a stated property has been proved against a formal model.

The bridge from mathematics to medical-device software is becoming concrete enough to inspect. In February 2026, Leo de Moura described an experiment in which Kim Morrison at the Lean Focused Research Organization used Claude to convert the production C compression library zlib into Lean and produce a machine-checked proof of roundtrip correctness. The claim was limited but operational: compressing and then decompressing returns the original data, as expressed in Lean and checked by Lean’s kernel.[1]

That is the kind of result worth slowing down for. zlib is not a toy benchmark invented to make theorem proving look good. It is ordinary infrastructure. The proof did not establish every desirable property of the library, and it was one experiment rather than a general result about all C programs. Still, it shows the relevant shape of the work: use an AI system to help translate implementation behavior into a formal environment, then let the theorem prover check whether the proof actually closes.

Why the zlib proof is a better starting point than the math headlines

The math headlines are not irrelevant. They show that AI systems can search spaces that were previously too large or too tedious for human proof engineering alone. But for a hospital, a device manufacturer, or a reviewer reading a safety case, an open conjecture is still one step removed from the hard question: can this method say anything enforceable about software that touches patients?

The zlib example gives a more direct answer. It points to a workflow in which a general-purpose model proposes formal material and the proof assistant refuses to accept it unless it type-checks. That is a different trust posture from “the model explained itself well.” The system has to satisfy a checker whose job is not to be impressed.

Lean also has escaped the small-demo category. De Moura’s account notes that AWS uses Lean to verify the Cedar policy engine, Microsoft uses it for SymCrypt, and Veil, a verifier for distributed protocols, is built on Lean.[1] Those examples do not prove that Lean is ready to certify clinical AI systems end to end. They do show that formal methods are already being applied to production systems where mistakes have security or reliability consequences.

That enterprise use is important because clinical AI safety is not primarily a philosophical problem. It is a systems problem with interfaces, inputs, updates, failure modes, operators, documentation, and evidence packages. A proof technique that only works in a clean mathematical sandbox would be interesting. A proof technique that can attach to real software components is more consequential.

What the conjecture-solving work actually contributes

The mathematics work supplies the precedent for scale. Quanta reported in April 2026 that the Lean ecosystem contained more than 200,000 formalized theorems and more than 750 contributors, with systems including AlphaProof, Aristotle, SEED Prover, Axiom, Aleph, and Mistral AI using or interacting with that environment.[2] That matters less as a sociology of mathematics than as infrastructure: a growing library of formal facts gives AI proof search something stable to build on.

The AlphaProof Nexus paper is more specific. It reports that the system autonomously solved 9 of 353 open Erdős problems, with inference costs in the range of $60 to $600 per problem.[3] The dollar amounts should not be mistaken for the full cost of doing formal work; they do not include the human labor behind the environment, the benchmarks, or the surrounding research program. But they do make one point hard to ignore: proof search that once looked artisanal is becoming more automatable.

For clinical AI, the analogy is not that a theorem about number theory resembles a radiology model. It does not. The analogy is procedural. A conjecture must be stated precisely enough to be checked. A proof must be reduced to steps accepted by a formal system. The same discipline could be applied to bounded properties of clinical AI software: data-handling invariants, access-control behavior, update constraints, alarm logic, fallback rules, or guarantees about a preprocessing pipeline.

Those are not the whole safety case. They are the parts where “every possible input covered by the model” means something. Testing can sample representative cases. Formal verification can, in the right conditions, exhaust the state space described by the specification.

The trust problem moves into the specification

Formal verification is often described as if it removes trust. It does not. It relocates trust.

A verified property is only as useful as the formal statement being verified, the model of the system, the assumptions about the environment, and the correctness of the tooling base. In software engineering, that can still be an excellent trade. “This parser never reads past this buffer under these assumptions” is a meaningful property. “This policy engine enforces this access rule for all requests expressible in this language” is a meaningful property. These claims are narrower than “the system is safe,” but they are stronger than “we tested many examples and did not see a failure.”

Clinical AI makes the specification problem harder. A classifier’s intended behavior may depend on image quality, disease prevalence, reader workflow, patient subgroup, site-specific acquisition protocols, and the consequences of false reassurance. A triage model may be judged not only by whether it produces the same output for a given input, but by whether the output is clinically useful under timing pressure. A monitoring algorithm may need to trade sensitivity against alarm fatigue. Those are not impossible to formalize in pieces, but they are not waiting around as clean mathematical predicates.

This is where a compliance-minded team should be most interested and most suspicious. The proof assistant can enforce rigor after the property is written. It cannot decide, by itself, whether the property captures the clinical obligation the manufacturer owes to the patient, the operator, or the institution deploying the system.

A proof can fail in ways that look familiar

The AlphaProof Nexus paper is useful partly because it reports failure, not just success. Its analysis found that top-scoring AI proofs frequently relied on hallucinated lemmas, including nonexistent “established results.”[3] That is not the same failure mode as an ordinary chatbot inventing a citation in a clinical answer, but it is close enough to make the warning legible.

The formal system narrows the damage. A nonexistent lemma cannot simply pass through Lean if the proof is actually checked against available definitions and theorems. But hallucinated intermediate structure can still waste reviewer time, distort the search process, or tempt humans to accept a statement that has not been grounded correctly. In a clinical setting, the parallel risk is not merely “the model lies.” It is that an AI-assisted verification workflow may produce the wrong formal target, rely on an assumption that is clinically invalid, or verify a simplified surrogate while the deployed system fails somewhere else.

Kevin Buzzard of Imperial College put the mathematical version bluntly: “One hallucination can break an entire mathematical argument because that's the nature of mathematics.”[2] Clinical reasoning is not identical to mathematics, but safety cases have the same brittleness at their load-bearing joints. One invalid assumption about input distribution, reader behavior, missingness, or update control can make an otherwise careful argument point at the wrong system.

Where formal proof could help clinical AI first

The most plausible early uses are not sweeping claims that a diagnostic model is clinically safe. They are bounded claims around software behavior, control logic, and lifecycle constraints. That is not a retreat. It is how verification becomes useful without pretending to answer questions it has not been given in formal form.

These are the kinds of properties that already resemble production software verification more than open-ended clinical judgment. They also map to the parts of AI-enabled medical devices that tend to become painful during audits: what changed, who approved it, what data were accepted, whether a fallback executed, whether the system’s behavior matches the documentation, and whether an edge case was merely untested or actually impossible under the specification.

For radiology AI, for example, formal proof would not eliminate the need for clinical validation. Evidence gaps in existing device evaluations remain a separate problem, especially where performance claims depend on prospective clinical use rather than software invariants. That distinction is why discussions of FDA-cleared radiology AI evidence gaps should not be collapsed into discussions of theorem proving. A verified pipeline can strengthen confidence that the right computation runs. It cannot, by itself, show that the computation improves care.

Why healthcare should care now, even if the pathway is immature

The timing is not accidental. De Moura’s post states that AI writes 25% to 30% of new code at major technology firms and that nearly half of AI-generated code fails basic security tests.[1] Those figures are not medical-device-specific, but the direction of travel matters. If AI accelerates code production faster than organizations can review, test, and document it, the quality system inherits more surface area.

Medical device software is not exempt from that pressure. Teams already have to manage conventional software defects, third-party dependencies, cybersecurity expectations, human-factors constraints, and post-market obligations. Add AI-generated code, AI-generated tests, AI-generated documentation, and AI-assisted model updates, and the review burden does not shrink just because the artifacts arrive faster.

Formal verification offers a way to make some of that burden more mechanical. If an AI system generates code and another AI system helps generate a proof, the safety value still comes from the independent checker and the inspectable specification. The regulator, manufacturer, or hospital does not need to believe the model’s prose. They need to know what property was stated, what assumptions were made, what artifact was checked, and what remains outside the proof.

Proof and testing answer different regulatory questions

Current FDA practice for AI/ML software as a medical device is still organized around evidence, lifecycle management, change control, transparency, and post-market monitoring. Predetermined Change Control Plans fit that logic: define what can change, how it will be controlled, and how performance and safety will be maintained after authorization. That framework can become more adaptive than a one-time clearance, but it remains testing-based and lifecycle-based rather than proof-based.

That is not a criticism of the FDA for failing to behave like a theorem prover. Clinical safety cannot be reduced to formal software properties. A device may satisfy every verified invariant and still perform poorly for a subgroup, degrade under site-specific workflow, or cause harm because humans overtrust its output. Empirical testing, clinical validation, usability assessment, monitoring, and adverse-event processes remain necessary because they observe the system in the world rather than inside a formal model.

The better comparison is narrower. Testing asks whether selected cases behaved acceptably. Formal verification asks whether a specified property holds for all cases within a modeled space. A PCCP asks how future changes will be controlled and assessed. A proof could support part of that control story by showing, for example, that an update mechanism cannot deploy an unapproved model or that a monitoring rule always triggers a required fallback when a defined condition occurs.

That is why formal methods fit best as a supplement to the current regulatory evolution described in From Evidence Gaps to Lifecycle Oversight. They could make parts of a lifecycle claim stronger. They do not turn a lifecycle framework into mathematical certainty.

No formal-verification pathway exists yet for AI/ML medical devices

It is important not to overstate the regulatory status. The available materials do not show that the FDA has issued a formal-verification pathway for AI/ML medical devices. A manufacturer could use formal methods as part of its engineering evidence, but that is different from saying there is an established route in which a Lean proof substitutes for clinical validation or recognized performance testing.

If formal proof enters review more seriously, the first questions should be ordinary and demanding: What exactly was specified? Which version of the software was modeled? How was the model connected to the executable artifact? Which assumptions concern the deployment environment? Which safety claims still depend on empirical evidence? Who can reproduce the proof? What happens when the model changes?

Those questions sound less exciting than “AI solved an open conjecture.” They are also the questions that determine whether proof becomes regulatory evidence rather than technical theater.

The credible roadmap is modular

A realistic roadmap for clinical AI verification starts with components whose behavior can be specified cleanly. It does not start with a claim that the entire clinical act can be proved safe. That means treating formal proof as one layer in a safety case.

• Use formal verification for deterministic software properties where exhaustive coverage is meaningful.
• Use empirical validation for clinical performance, subgroup behavior, workflow effects, and benefit-risk claims.
• Use lifecycle controls for model updates, monitoring, rollback, and documentation continuity.
• Use post-market evidence for drift, misuse, unexpected deployment conditions, and harms not captured before release.

The hierarchy matters because the pressure on regulators and manufacturers is growing. More AI devices entering the market means more claims to assess, more updates to track, and more places where sampled testing may miss a consequential edge case. The growing scale of AI device authorizations makes stronger verification tools attractive, but scale alone does not relax the need to match each method to the kind of claim it can actually support.

Mathematical conjecture solving contributes confidence that AI-assisted proof search can be more than a parlor trick. The zlib proof contributes confidence that the method can touch production software. Enterprise Lean use contributes confidence that serious systems teams are willing to invest in this infrastructure. The AlphaProof hallucinated-lemma failures contribute the necessary warning: the AI layer can still corrupt the reasoning process unless the formal boundary is enforced and the specification is inspected.

That leaves a bounded but useful conclusion. Formal verification is a credible roadmap for clinical AI safety when the target is a well-specified property of a well-modeled system. It is not a replacement for clinical evidence, and it is not a machine for manufacturing regulatory certainty from ambiguous goals. The practical question is therefore not whether proof can make clinical AI safe in one step. It is what can be verified today, what still has to be tested in patients and workflows, and where a formal specification can make the safety case harder to hand-wave.

References

1. When AI Writes the World's Software, Who Verifies It? — Leo de Moura blog, Feb. 28, 2026.
2. The AI Revolution in Math Has Arrived — Quanta Magazine, Apr. 13, 2026.
3. Advancing Mathematics Research with AI-Driven Formal Proof Search — arXiv 2605.22763v1.