AI Is Discovering New Mathematics. The Hard Part Is Knowing Exactly What It Proved.

What mathematical breakthroughs reveal about turning human knowledge into dependable software.

Compile-Time Intelligence, Part 1

Something extraordinary is happening in mathematics.

AI systems are moving beyond solving difficult problems whose answers humans already know. They are beginning to contribute original arguments to open research questions, including problems that have resisted mathematicians for years.

In February 2026, Google DeepMind’s Thang Luong and Vahab Mirrokni reported autonomous AI solutions to four open Erdős questions. In August, OpenAI announced ten advances spanning mathematics and theoretical computer science, including claimed progress on long-standing problems in group theory, combinatorics, and computational complexity. And on October 6, OpenAI released 722 mathematical manuscripts produced by an internal frontier model. [1] [2] [3]

These results are at different stages of validation. OpenAI’s first update included corrections and withdrawals, and reported that about 42% of the remaining manuscripts had their main result formalized for computer checking. Proposed breakthroughs still need scrutiny. But the broader development is remarkable: AI is becoming a serious participant in the creation of mathematical knowledge. [3]

But how do we harness this capability reliably?

A central part of the answer lies in something deceptively difficult: connecting the language in which humans express ideas with the formal logic in which computers can verify them.

That challenge extends well beyond mathematics. Consider clinical guidelines, legal agreements, insurance policies, or lending rules. A model may be able to read these documents and generate executable logic. Establishing that the logic preserves their meaning is another task.

The recent launch of Compiled Health brings that ambition directly into patient care. The company is working to turn medical standards into deterministic, traceable decision logic that can run in the software clinicians already use. Imagine what that could mean for patients: a dangerous change in someone’s condition recognized earlier, a contraindication caught before a treatment is recommended, or evidence-based guidance applied consistently even in an overstretched clinic. Getting this right could help turn decades of accumulated medical knowledge into better decisions at the moment they matter most. But the stakes run both ways. If a threshold, exception, or clinical qualification is mistranslated, a widely deployed system could repeat that error across thousands of patient decisions. [4]

This is the central question I want to explore: as AI begins discovering new mathematics and turning human knowledge into executable decisions, how do we ensure that the formal logic a machine can verify actually captures what humans intended?

The answer takes us from mathematical proofs to clinical decisions, and into one of the most important engineering challenges in AI: making the translation between human meaning and machine-executable logic reliable enough to trust.

The power of a proof we can check

To understand how these mathematical results can be checked rigorously, it helps to follow the path from a human question to a machine-checked proof.

In a research paper, a mathematical claim and the argument supporting it are expressed through human language, notation, and conventions that other mathematicians understand. A proof checker needs the claim expressed as a formal statement, with precisely specified definitions and assumptions, and a formal proof establishing it. That proof may be a translation of an existing written argument, or it may be discovered directly within the formal system.

These are two distinct tasks: expressing the intended claim correctly and establishing it. The checker verifies that the formal proof establishes the formal statement. Whether that statement captures the original question, or whether the proof faithfully represents a particular written argument, requires separate scrutiny.

Google DeepMind’s AlphaProof (led by Thomas Hubert, Rishi Mehta, and Laurent Sartran, with Eric Wieser among its key contributors) and AlphaGeometry 2 solved four of the six problems from the 2024 International Mathematical Olympiad, achieving a silver-medal-equivalent score. [5]

AlphaProof learned to find formal proofs through reinforcement learning, training on millions of automatically formalized problems. It worked in Lean, a proof assistant: software that checks whether a mathematical proof establishes a stated theorem from its definitions and assumptions. Successful proof attempts provided feedback for further learning. [6]

Machine checking already existed. AlphaProof’s advance was learning to find proofs within that environment at Olympiad-level difficulty. The combination is powerful because the system can search for an argument while Lean checks whether the argument establishes the formal claim.

But there is an important detail. Human experts first translated the Olympiad problems into formal mathematical language. Lean checked AlphaProof’s proofs against those translations, not against the original problem descriptions. [5] [6]

If the translation changes what the problem asks, Lean can approve a valid proof of the wrong statement.

A recent controversy shows why this distinction matters.

In September, OpenAI announced a claimed proof of finite-time blow-up for the three-dimensional Navier–Stokes equations with smooth external forcing. It presented the result as establishing statements (C) and (D) of the official Millennium Prize formulation, and released both a written argument and Lean formalizations. [7]

But then in October, Navier–Stokes Lost in Translation (Alexander Bastounis, Fabian Circelli, and Anders C. Hansen) identified discrepancies between portions of that written argument and their formal counterparts. One estimate in the paper used four additional input derivatives; the corresponding Lean estimate used five, yielding a weaker bound. Another differed in both its statement and its proof strategy. [8]

The authors do not claim that the written proof is incorrect. Their finding concerns what the Lean formalization establishes about it. A formal proof might reach the intended final theorem through a different argument, without validating the particular argument presented to human readers.

That leaves two connections to examine: whether we formalized the right statement, and whether the formal proof corresponds to the explanation offered alongside it.

For systems that turn documents into software, the first connection is unavoidable. Before we can check a rule’s behavior, we need to establish that we have expressed the right rule.

Why translating a sentence is harder than it looks

At first glance, that sounds like a manageable problem. A model that can write code and reason about mathematics should be able to translate a sentence into logic.

Start with a simple benefits policy:

Full-time employees become eligible after at least twelve completed months of service.

For this illustration, assume these are the complete eligibility conditions, employment status is known, and completed months are counted as whole numbers.

One model produces:

full_time and completed_months >= 12

Another produces:

full_time and completed_months > 12

Both rules are well-formed. Both run. Both are satisfiable, meaning there are inputs for which each returns true.

For a full-time employee with eleven completed months, both say ineligible. With thirteen months, both say eligible. At exactly twelve months, they disagree.

The second rule is a mistranslation. Yet a test suite containing only the eleven- and thirteen-month cases would not reveal it.

Here, a human can spot the mistake quickly. The definitions, conditions, and boundary fit on one line. Real documents make the task harder in several ways.

A small change in logical structure can alter a claim. “Every employee has a manager who can approve their request” allows different managers for different employees. “There is one manager who can approve every employee’s request” requires a common approver. Preserving the vocabulary while changing that structure changes the rule.

Meaning can also depend on material elsewhere in the document. An eligibility condition may be qualified by an exception several pages later. A term may have a technical definition that differs from its everyday meaning. A mathematical statement may rely on conventions that its author expects every reader to supply.

Even carefully maintained mathematical formalizations encounter these problems. Formal Conjectures (Moritz Firsching, Eric Wieser, and colleagues) reports 291 corrected misformalizations. Most involved misrepresenting the source or mishandling the semantics of Lean’s types and operations; a smaller group involved implicit conventions. These are corrections in a collaborative research repository, not an error rate measured for a single model. [9]

The difficulty therefore has two sides. Sometimes the source is clear and the translation gets it wrong. Sometimes the source itself needs clarification. Formal Conjectures describes how attempts to formalize Erdős Problem 978 prompted a refinement of the informal question. [9]

Outside mathematics, leaving room for interpretation can be intentional.

Suppose a policy says a request should be handled “promptly.” Converting that to “within 24 hours” produces an executable deadline, but the number has to come from somewhere. Unless another source supplies it, the translator has made a policy decision.

Likewise, an instruction to “consider” a treatment preserves a choice. Automatically ordering the treatment would remove that choice. A system could present the option for clinical assessment, but even requiring that assessment to be documented would be an additional workflow requirement.

Now imagine translating a clinical guideline for choosing a treatment. The recommendation might depend on a patient’s age, kidney function, other diagnoses, current medications, recent test results, and exceptions defined elsewhere in the guideline. Each factor introduces further questions. Which laboratory measurement should be used, and how recent must it be? Which contraindications override the general recommendation? What happens when required information is missing, or when two recommendations conflict? The possibilities multiply because these decisions interact: choosing one interpretation can change which other rules apply. And the system must work across the many combinations of patient conditions and available evidence, not just a typical example. A model might generate a perfectly reasonable rule for one patient while missing an uncommon but critical combination. The real challenge is to preserve the meaning of an entire decision process, including its qualifications, exceptions, and unresolved questions, rather than simply turn an isolated sentence into executable code.

This is why autoformalization, the translation of informal statements into formal representations, is an important research problem. It requires preserving logical structure, finding context, understanding the target representation, and recognizing decisions the source does not authorize the translator to make.

A model can produce something precise by filling in those gaps. Precision alone does not tell us whether it filled them correctly.

How to examine the translation itself

Once we separate these problems, the role of verification becomes clearer.

The first task is to check properties of the generated logic. The second is to gather evidence that this logic represents the source. Formal methods can help with both, but the questions we ask them must differ.

Beyond Solver Verdicts (Vikash Singh, Ali Torkamani, Ferhat Erata, and colleagues) examines a specific information limit. The researchers show that, on matched pairs of translations with identical binary solver verdicts, one logically equivalent to a designated reference and one not, a score using only that verdict cannot distinguish them better than chance. The limitation concerns what can be learned from the verdict alone. [10]

Our benefits example makes the point concrete. Asking whether each rule is satisfiable returns “yes” twice. The answer contains no information about the difference at twelve months.

Instead, we can ask whether there is any allowed input on which the two rules disagree. For this simple representation, a solver can find the full-time employee with exactly twelve completed months.

That is a useful division of labor. The solver exposes the disputed case. A reviewer returns to the policy and establishes the intended answer.

Where an independently validated formal reference exists, the comparison can go further. An equivalence check can establish that a candidate matches the reference within the modeled domain and assumptions. A timeout or “unknown” result leaves the question unresolved.

AlphaProof’s team used this approach to improve its formalizer. On a subset of problems with ground-truth Lean statements, generated examples were added to training when their equivalence to the reference could be proved. The reference itself still had to represent the original problem correctly. [6]

Other methods provide evidence when a reference is unavailable for a new case. Beyond Solver Verdicts trains a learned verifier using labels from equivalence checks against references. Once trained, it examines the source text and candidate formalization without needing a reference at deployment. Its predictions estimate agreement with the reference-based target; they are empirical assessments, not mathematical guarantees of intended meaning. [10]

Stratified Consistency Distillation (Zhichao Hou, Ferhat Erata, Joe Lilien, and Ali Torkamani) approaches the problem through multiple translations. Its training pipeline generates ten candidates per input, groups them by logical equivalence, and uses their agreement structure to select or construct training examples for a smaller model. [11]

That is a training method, but it suggests a useful review strategy: identify cases where candidate translations disagree, then show reviewers the consequences of choosing one over another.

Agreement still needs scrutiny. Several samples can share an error, and disagreement may reflect a model mistake rather than genuine ambiguity in the source. The value lies in combining this signal with independent examples, formal comparisons, and domain expertise.

The result is a more productive question than “Did the generated code pass?”

It is: “What evidence supports this particular translation?”

What changes when the checker runs in production

So far, we’ve been discussing how to establish that a formal rule faithfully represents its source. But once that rule is deployed, a different problem arises: applying it correctly to each individual case.

Imagine an AI benefits assistant answering an employee’s question about eligibility. The employee supplies their employment status and length of service, and the assistant proposes an answer: “You’re eligible.” Before that answer is used, a checker can evaluate whether it follows from the company’s formalized policy, given the information supplied about this employee. If the conclusion is supported, the application may allow it to proceed. If it contradicts the policy, the answer can be blocked or corrected. And if the information is insufficient, or the system cannot interpret the claim reliably, the case can be sent for clarification or human review.

Now imagine that happening across thousands of individual interactions, each involving different circumstances. The checker repeatedly applies the same approved policy to new premises and claims. It does not independently establish that the employee’s reported information is accurate, and it does not revalidate the original policy translation with every request. Those require separate controls. The system around the checker must decide what each result means, when an automated action is permitted, and when a person needs to intervene.

Amazon Bedrock’s Automated Reasoning checks provide an example. The associated paper (coauthors include Rémi Delmas, Ferhat Erata, Ali Torkamani, Byron Cook, and Darion Cassel) describes a system that formalizes policies and checks statements against them. A policy can be reviewed before reuse; at runtime, models translate the premises and claims in an answer, and a solver evaluates them against that policy. [12]

The distinction between premises and claims is important. A VALID finding establishes that the translated claim follows from the formalized policy and the translated premises. It does not establish that those premises are true in the world, and it does not validate claims left untranslated. [13]

AWS also documents fidelity reports that connect extracted rules and variables to source statements, helping reviewers examine coverage and translation quality. These are part of reviewing the policy, rather than a mathematical proof that the source was interpreted correctly. [13]

The paper’s evaluation shows why the meaning of an approval must be measured carefully. Using automatically generated, unvetted policies, the researchers ran 563 cases three times each, producing 1,689 decisions. In the selected configuration, each evaluation also used three redundant translations, requiring agreement across all three before logical validation. Across the 1,689 decisions, the system returned 179 VALID findings, ten of which were incorrect: 94.4% precision. The system confirmed 14.9% of genuinely valid answers. [12]

Its reported empirical “soundness” was 99.4%, calculated using all decisions as the denominator for incorrect approvals. That metric and approval precision answer different questions; the authors also report recall because their soundness measure rewards abstention. [12]

For a team deploying such a system, those distinctions affect the workflow. What evidence must be checked before an approval can trigger an action? What happens to untranslated content? Who resolves an ambiguous finding?

The opportunity is substantial: formalized policies can be reused, checked, and inspected. Realizing that opportunity requires the surrounding system to preserve what each check establishes.

And in some domains, even a faithful reading of the source leaves a decision that has to be made before the rule can run.

When interpretation changes a clinical result

Healthcare makes that problem tangible.

The 2012 KDIGO definition of acute kidney injury includes a rise in serum creatinine to at least 1.5 times baseline, known or presumed to have occurred within seven days. The seven days concern the rise, not a universal limit on the age of the baseline measurement. [14]

The comparison looks simple. But which measurement represents the patient’s baseline?

A 2010 study by Edward Siew and colleagues examined that question in 4,863 hospitalized adults. Using an outpatient reference baseline, 25.5% were classified as having acute kidney injury. Using the admission value produced 13.7%; using the lowest value from the first seven hospital days produced 35.9%; and using a baseline back-calculated from an assumed kidney filtration rate of 75 mL/min/1.73 m² produced 38.3%. The study used the earlier AKIN criteria and predates KDIGO. [15]

The choice of input substantially changed the population identified.

These methods are not interchangeable clinical choices. A value measured later during hospitalization may be unavailable at admission. KDIGO describes the back-calculation approach for an unknown baseline provided there is no evidence of chronic kidney disease, and warns that unrecognized chronic disease can cause misclassification. [14]

A solver could verify that the threshold comparison behaves correctly for a fixed positive baseline. It could also identify patients whose classifications differ under alternative selection rules. Neither result would establish which selection procedure was appropriate for the clinical setting.

That requires an interpretation grounded in the guideline, the patient evidence, and clinical judgment. Authority matters too: KDIGO states that its guideline assists decision-making and does not itself define a standard of care or prescribe an exclusive course of management. [14]

This is where the architecture described by Compiled Health becomes relevant. Its approach places models at build time, where clinical knowledge is translated into artifacts that can be reviewed and versioned, and runs compiled artifacts at the point of care. [4]

That is the sense of compile-time intelligence explored in this series: using models while reusable logic is being constructed and examined, before that logic is deployed. Other architectures, such as AWS’s answer-checking system, perform some interpretation at runtime. The design question is which decisions can be settled in advance and what must still be evaluated for each new case.

Christian Chartier captures the clinical boundary in Reasoning Is Not Language: “what no compiler can prove is that the logic is the standard’s.” [16]

I read that as a reason to make the interpretation reviewable. The code can preserve an adopted clinical decision and execute it consistently. A proof about the code cannot supply the clinical judgment or authority that made that decision appropriate.

The practical challenge is therefore larger than generating the rule. We also need to preserve why that rule was chosen.

Keep the interpretation with the executable rule

This is where the research becomes an engineering approach.

Requirements engineers already maintain connections between requirements, implementations, and tests. Traceability is established practice, reflected in requirements such as NASA’s software engineering rules. [17]

Model-generated translation adds a scaling challenge. A team can produce candidate rules faster than specialists can inspect them. I would make the interpretation record part of the output from the start, so reviewers receive the source, proposed rule, assumptions, and supporting evidence together.

The record itself must be checked. A model-generated explanation of why a rule is correct is still a proposal.

For our fictional benefits policy, a compact record might look like this:

Source: “Full-time employees become eligible after at least twelve completed months of service.”
Rule: full_time and completed_months >= 12
Scope: These are the complete eligibility conditions in this illustration. Employment status and completed months are known.
Reason for the boundary: “At least twelve” includes exactly twelve.
Rejected translation: full_time and completed_months > 12, which incorrectly excludes the twelve-month case.
Expected outcomes: Full-time at 11, 12, and 13 months: no, yes, yes. Part-time at 12 months: no.

These are expected test outcomes, not results from a production implementation. Before release, the responsible policy owner would approve the interpretation and the implementation would be tested against those expectations.

The same structure becomes more valuable as the rule becomes more complex. A clinical baseline record would need the source version, selection procedure, applicable population, permitted evidence, decision-time constraints, and review authority. It should distinguish requirements stated in the source from assumptions or local adaptations introduced during implementation.

It should also preserve unresolved questions.

A clear rule with missing patient data is different from a guideline whose meaning has not yet been settled. The former may require another measurement or a request for information. The latter may require an authorized interpretation before the affected rule is released. Treating both as “false” would hide the reason the system cannot decide.

The benefit becomes especially clear when something changes.

Suppose a policy changes its eligibility threshold. With the source, rule, and tests connected, the system can identify the affected logic, generate a proposed revision, and show which cases would receive different answers.

Suppose instead that a new model produces a different translation of an unchanged policy. The difference becomes something to investigate against the approved interpretation, rather than a reason to silently replace it.

This also gives increasingly capable models useful work to do. They can identify cross-references, propose competing readings, generate cases that distinguish them, and help reviewers inspect the consequences. Disagreement can focus specialist attention, while independently selected tests provide coverage beyond the differences the models happen to find.

The interpretation connecting the source to the executable artifact should remain visible, testable, and open to challenge.

That is what lets a team improve the model without losing track of the decisions the organization has already authorized.

From discovering knowledge to putting it to work

AI’s emerging contribution to mathematics is exciting because it expands what we might discover. Formal verification gives us a powerful way to examine those discoveries. Connecting a checked result to the question humans intended is part of making the achievement useful.

The same connection matters when the knowledge already exists. A clinical guideline or lending policy has to retain its qualifications, exceptions, and authority as it becomes software. Otherwise, greater consistency can simply mean applying the wrong interpretation more consistently.

I think this is one of the most consequential engineering opportunities around increasingly capable models. Better models can do more of the work of discovery and interpretation. Better verification and review systems can make the results easier to inspect, reuse, and maintain.

The aim is to bring those capabilities together: a model that can propose something valuable, checks that establish precise properties, and a record that explains why the result answers the intended question.

In mathematics, that helps turn a proposed argument into knowledge others can examine and build on. In a clinical or enterprise workflow, it helps turn written knowledge into behavior an organization can justify.

Part 2 takes up a practical problem within that process: how to design tests that distinguish plausible-looking rules when no trusted formal reference already exists.

Building a system that turns policies, contracts, or clinical guidance into executable logic? Talk to Eventum about designing the translation, evaluation, and review process around it.

Sources

1. Luong T, Mirrokni V. Accelerating Mathematical and Scientific Discovery with Gemini Deep Think. Google DeepMind, February 11, 2026.
2. OpenAI. Ten advances in mathematics and theoretical computer science. August 1, 2026.
3. OpenAI. Sharing AI progress in mathematics. October 6, 2026; accompanying mathematics repository and revision history. The October 7 update records three withdrawals following a sign error, revisions to 14 other manuscripts, and 300 principal results formalized among the remaining 719 manuscripts.
4. Compiled Health. The standard of care applied deterministically. Company website; accompanying public launch announcement on the company’s LinkedIn page.
5. Google DeepMind. AI achieves silver-medal standard solving International Mathematical Olympiad problems. July 25, 2024. Includes AlphaProof leadership and contributor acknowledgements.
6. Hubert T, Mehta R, Sartran L, et al., including Eric Wieser. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature 651, 607–613 (2026); published online November 12, 2025. DOI: 10.1038/s41586-025-09833-y.
7. OpenAI. On the Navier–Stokes Millennium Prize Problem. September 8, 2026. The announcement claims proofs of statements (C) and (D) of the official formulation and links the written argument and Lean artifacts.
8. Bastounis A, Circelli F, Hansen AC. Navier–Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs. arXiv:2610.08144, version 1, October 6, 2026. Preprint; especially §§3.1–3.2.
9. Firsching M, et al., including Eric Wieser. Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics. arXiv:2605.13171, version 1, May 2026. Preprint; especially §3.3 and Table 5.
10. Singh V, Ganguly D, Goel A, Torkamani A, Han X, Lilien J, Erata F, Chaudhary V. Beyond Solver Verdicts: Generative Reward Models for Autoformalization. arXiv:2609.11085, version 2, September 2026. Preprint.
11. Hou Z, Erata F, Lilien J, Torkamani M. Stratified Consistency Distillation for Natural Language Formalization. arXiv:2608.30258, first submitted August 2026; version 3, October 2026. The author identified as Ali Torkamani in the article is listed as MohamadAli Torkamani in this paper. Preprint.
12. An C, et al., including Darion Cassel, Byron Cook, Rémi Delmas, Ferhat Erata, and Ali Torkamani. A Neurosymbolic Approach to Natural Language Formalization and Verification. Extended arXiv version 2511.09008v2. Numerical results cited here are from Table 1.
13. Amazon Web Services. Automated Reasoning checks concepts. Amazon Bedrock documentation, including the fidelity report, translation fields, and validation-results reference.
14. KDIGO Acute Kidney Injury Work Group. KDIGO Clinical Practice Guideline for Acute Kidney Injury. Kidney International Supplements 2 (2012), especially recommendation 2.1.1, chapter 2.4, and the guideline’s notice concerning its use.
15. Siew ED, Matheny ME, Ikizler TA, et al. Commonly used surrogates for baseline renal function affect the classification and prognosis of acute kidney injury. Kidney International 77(6), 536–542 (2010). DOI: 10.1038/ki.2009.479.
16. Chartier C. Reasoning Is Not Language. July 19, 2026.
17. NASA. Software Engineering Handbook, SWE-052: Bidirectional Traceability. Explains the requirements in NPR 7150.2D, §3.12.1, including their applicability by software classification.