After Proofs Become Machine-Checkable: AI-Originated Mathematical Results, the Lean Chain of Trust, and the New Gate of "Statement Faithfulness" (Deep Dive)

1. Background: A Few Necessary Concepts

3-SAT and ETH. A 3-SAT problem gives a logical formula made of clauses, each an "OR" of at most three variables (or their negations), joined by "AND," and asks whether some true/false assignment makes all clauses hold. Checking an answer is easy, but the time known algorithms need grows exponentially with the number of variables n. According to Papex's summary of the Anthropic paper, the previous records were about 1.328ⁿ for deterministic algorithms and about 1.308ⁿ for randomized ones [3]. The Exponential Time Hypothesis (ETH), proposed by Impagliazzo and Paturi, asserts that there is some fixed constant δ > 0 such that no algorithm can solve 3-SAT in 2^(δn) time — the base can shrink, but the running time cannot escape the exponential. A large number of "conditional lower bounds" rest on ETH [1][3].

Refuting ETH does not mean P = NP. Refuting ETH means 3-SAT can be solved in "subexponential" time, e.g., 2^(n/√log n), which is far less than 2ⁿ but still far more than any polynomial. Both companies' papers state explicitly that the result does not directly bear on P vs. NP and yields no practical algorithm [2][3].

Lean and the "kernel." Lean is an interactive theorem prover. After a person or an AI writes a proof, a very small "kernel" program checks step by step whether each inference is legal. A small kernel is easier to review and to trust. Proofs also rely on a few "axioms"; Lean's standard axioms are propositional extensionality (propext), the axiom of choice (Classical.choice), and quotient soundness (Quot.sound) [2]. On the soundness of Lean's type theory itself, an October theoretical work further proves that a formula in the language of second-order arithmetic is provable in "ZFC + infinitely many strongly inaccessible cardinals" if and only if it can be constructed as a type in Lean [11] — a finer mathematical characterization of "what Lean proves."

Technical lineage: from "machines checking human proofs" to "machines proposing new results"

"AI doing mathematics" did not start in October. Connecting a few threads reveals three stages.

Stage 1: formalization as a checking tool. Take the classification of finite simple groups. According to Axiom's retrospective, in 1963 Feit and Thompson proved that every nonabelian finite simple group has even order, in a 255-page paper that filled an entire issue of the Pacific Journal of Mathematics; in 1983 Gorenstein announced that the classification was complete; and the remaining quasithin gap was closed only in 2004, by Aschbacher and Smith's 1,221-page treatment [4]. On the formalization side, in 2012 a team led by Gonthier completed a formalization of the Feit–Thompson theorem in Coq (now Rocq) after a six-year effort, an early demonstration that a proof of such depth could be fully machine-checked [4]. The hallmark of this stage: humans write the proof first, and machines spend years checking it.

Stage 2: AI enters "problem solving" and "proof filling." Competition-level theorem-proving benchmarks have steadily fallen; Maestro, discussed below, proves 669 of 672 problems on PutnamBench [7]. As benchmarks near saturation, researchers turn to harder, less leakage-prone evaluations, such as ReuF2F, which collects open problems from undergraduate research projects [12]. Meanwhile, formalization tools are being redesigned around "humans supervising agents": the Numina Fuse authors used their system in the formalization of the three-dimensional Kakeya conjecture [8], which Wang and Zahl proved in 2025 [1].

Stage 3 (October 2026): AI produces new results, and formalization becomes the release threshold. OpenAI had already released a result on October 6 by "publishing the AI output directly," and its three results on October 26 followed and extended that approach [1]. The local smoothing conjecture had previously been proved only in two spatial dimensions, by Guth, Wang, and Zhang in 2019; this time OpenAI says its models produced a proof in every dimension [1]. Axiom's CFSG project pushed "checking" to an entirely new scale: building on earlier Lean work, including about 1.2 million lines of code from Qiuzhen-CFSG, it formalized the entire classification theorem in 24 days [4]. From "years to check one theorem" to "weeks to formalize a body of theory," and then to "the model proposes a result and attaches a Lean proof right away," the bottleneck has shifted from "the proof cannot be written" to "is the stated proposition faithful, and who reviews it?"

2. What Happened: The Facts

OpenAI's three results (2026-10-26) [1]:

• Mathematics: The model gave a proof of the local smoothing conjecture, posed by Sogge in 1991, in all dimensions, based on a new auxiliary partial differential equation; the conjecture implies the Kakeya conjecture and Stein's restriction conjecture. OpenAI says it obtained the output on October 18, completed the Lean formalization the next day, and released both the natural-language manuscript and the Lean proof. Papex notes that the paper's own statement about the restriction conjecture is narrower ("in the interior of the conjectured range"), and whether it covers all forms is for experts to judge [3].
• Computer science: OpenAI says its system found a natural-language refutation of ETH on October 16 and completed the Lean formalization on October 17. A group led by Impagliazzo, Paturi (UC San Diego), and Williams (MIT) is organizing a public review. The three reviewers wrote in an open letter: "Our involvement should not be read as a certification of the result." [3]
• Physics: The model produced natural-language proofs of pure Yang–Mills existence and QCD existence on September 9 and September 18 respectively, and completed the Lean formalization of Yang–Mills existence on October 16; a group led by Gross is handling the follow-up and is not yet releasing the AI-produced material. Papex stresses that this result concerns existence and does not address the "mass gap" part of the Millennium Prize problem [3].

OpenAI also set out four principles for external collaboration — transparency, not seeking academic authorship, crediting those who curate the work, and independence — and mentioned its USD 5 million grant to the Simons Foundation [1].

Anthropic's ETH refutation (2026-10-27 UTC) [2]: The repository states that a deterministic algorithm solves 3-SAT in 2^o(n) time; in fact, it counts the satisfying assignments of 3-SAT (#3-SAT) in 2^O(n·log log n/√log n) time. The repository says explicitly: "This result is purely asymptotic and says nothing about solving formulas in practice." According to Papex, the Anthropic paper says the core algorithm was found by an internal Claude research model on October 16 — "14 million output tokens, no human input" — and that the two results were obtained "independently and simultaneously"; the paper also estimates that practical gains are unlikely to appear "unless n > 10⁷" [3]. The two papers give the same leading exponent; OpenAI's Lean scope note says its formal proof gives a weaker exponent of n(log log n)²/√log n [3].

Axiom's CFSG formalization (2026-10-26) [4]: The Classification of Finite Simple Groups is considered the longest mathematical proof ever written by humans — about 15,000 pages, more than 500 papers, roughly 100 mathematicians. Axiom says the team started on October 1, building on existing Lean work and an internal "proof map," and divided the project into 108 milestones and about 380 small tasks; dozens of AI agents produced about 43.1 million lines of Lean code in 24 days; on October 10 they proved that the Monster is simple. The formalization uncovered 34 "notable discrepancies." The most important concerns the Unbalanced Group Theorem (UGT): agents found an explicit counterexample to a closure assertion in Walter's 1986 proof, and the team rewrote the proof route. Another comes from Aschbacher and Smith's "quasithin" volumes: a lemma asserts two quantities are equal, and agents found a counterexample using SL₂(5) (one quantity is 1 where the equation requires 2), changed the equality to an inequality, and completed the affected arguments. Original contributors consulted included Lyons and Solomon.

Axiom's engineering details are equally noteworthy [4]. First, "assumption creep": some early milestones that looked manageable actually depended on many unproven premises that agents assumed to hold; the team deleted tens of thousands of lines built on these assumptions and restarted parts of the work on a sounder plan. Second, the build bottleneck: agents produced proofs faster than Lean could recheck them, and changing one shared result forced everything depending on it to be rechecked; the team built a system that distributes build caches across machines and checks independent results in parallel, and moved expensive finite computations out into separately checkable "certificates," speeding verification up by several orders of magnitude. Third, replanning: on October 13 only one milestone was closed, so the team had agents break unfinished milestones into smaller, precisely stated theorems, requiring each decomposition to explain how the small theorems combine into the original milestone through a short Lean proof. These three points — managing assumptions, incremental verification, and traceable task decomposition — are instructive for any large-scale multi-agent project.

The dispute over how to publish. OpenAI used three different release strategies for its three results: release the AI output directly for the mathematics result; release the output and convene an external review group for the computer-science result; and let an external group decide when to release for the physics result [1]. Anthropic took a fourth route: publishing the paper and Lean proof directly on its own GitHub and archiving them on the Hexagon mathematics preprint server, declaring them "primarily AI-generated" and "partially checked and understood by humans" [3]. According to Papex, the Advisory Group on Mathematics and AI (AGMAI) at the Institute for Advanced Study in Princeton raised five concerns about "company-designated mathematicians acting as release gatekeepers" — delayed or unequal access, excluding other researchers from participating, selection bias, borrowed reputation, and needlessness — and called on OpenAI to release the natural-language and Lean outputs for Yang–Mills as soon as possible; AGMAI had earlier recommended that AI outputs be deposited in academic repositories not controlled by the publisher, with citable identifiers and change records, accompanied by the model name, prompts, chain of thought, number of attempts, compute, and cost [3]. At heart, this dispute is about who should keep the "provenance record" of AI research results, and at what granularity.

3. Mechanism ①: How Fast Is "Subexponential," Really?

One-line intuition: 2^o(n) means "the coefficient in the exponent tends to 0 as n grows," but it may tend to 0 extremely slowly — so slowly that at any realistic scale it is barely different from 2ⁿ.

Analogy: A product that "gets cheaper every year," but only by one ten-thousandth per year, will in theory eventually be cheap, yet you would barely notice within your lifetime.

Step by step:

1. Previous record: time about cⁿ (c ≈ 1.3), i.e., 2^(n·log₂c), with a constant exponent coefficient log₂1.3 ≈ 0.38.
2. ETH asserts: there is a constant δ > 0 such that every algorithm needs at least 2^(δn).
3. New result: time 2^(C·n·log log n/√log n); the exponent coefficient C·log log n/√log n tends to 0 as n grows, so for any fixed δ it eventually falls below δ once n is large enough — ETH fails.

Key formula:

T(n) = 2^( C · n · f(n) ),   f(n) = log log n / √(log n)
as n → ∞, f(n) → 0  ⇒  for any δ > 0, eventually C·f(n) < δ

• n: number of variables; T(n): upper bound on running time; C: an unspecified constant (the constant in big-O notation).
• f(n): the n-dependent coefficient in the exponent; it tends to 0, but very slowly.

Worked example (illustrative; base-2 logarithms, ignoring the constant C):

• n = 10⁶: log₂n ≈ 19.9, √log₂n ≈ 4.46, log₂log₂n ≈ 4.32, f(n) ≈ 0.97.
• n = 10¹²: log₂n ≈ 39.9, √ ≈ 6.32, log₂log₂n ≈ 5.32, f(n) ≈ 0.84.

So even at a trillion variables, the exponent coefficient is still close to 1; multiplied by the unknown constant C, it is quite likely worse than existing 1.3ⁿ-type algorithms. This is consistent in direction with the Anthropic paper's judgment that gains are unlikely to appear "unless n > 10⁷" [3], and explains why both companies stress "purely theoretical significance."

Why it matters, and when it "fails": Its significance is for the theoretical landscape — hundreds of conditional lower bounds premised on ETH lose their footing, and stronger hypotheses such as SETH fall with it (per Papex's summary of the OpenAI paper [3]); but some lower bounds can be derived from weaker hypotheses that may still hold. Its direct impact on engineering practice is close to zero, and any reading that "AI has made SAT solving faster" is a misreading.

4. Mechanism ②: The Lean Chain of Trust — How Many Gates Must a Proof Pass to Be "Believed"?

One-line intuition: "Verified in Lean" is not a single fact but a chain: Is the statement file faithful? Does the kernel accept the proof? Which axioms are used? Does it still pass with an independent kernel?

Analogy: For a contract to be trusted, it is not enough to be "fully signed and sealed" (kernel check); its terms must be what both parties agreed (statement faithfulness), it must contain "no hidden clauses" (axiom list), and "a second law firm's review finds no issue" (independent kernel).

Step by step (using Anthropic's eth project as the example [2]):

1. A short statement file: MainResults.lean states only "ETH is false" and the main theorem, contains no proofs, and depends only on Mathlib. The repository says explicitly: Lean checks the proofs, but no machine checks whether this file matches what the paper says, so the file is deliberately kept short for human readers to verify; an appendix of the paper lists the differences between the Lean statements and the printed ones.
2. Build and kernel check: pin the Lean and Mathlib versions (v4.33.1); a full build takes about 8 minutes (24 vCPUs, about 7 GB peak memory per process).
3. Axiom audit: print the axioms the two main results depend on; there should be only the three standard axioms propext, Classical.choice, and Quot.sound.
4. Statement comparison: use the Comparator tool to match the proved theorems one by one against the statements in a "challenge file," preventing "proving a quietly altered statement."
5. Independent kernel recheck: recheck the proof with a separately implemented kernel, nanoda, reducing the risk of a defect in a single kernel.

Pseudocode:

trust(project):
assert human_review(Statement.lean ≡ paper_claims)     # the one step that cannot be automated
assert lean_kernel_check(project) == OK
assert axioms(main_theorems) ⊆ {propext, Classical.choice, Quot.sound}
assert comparator(Statement.lean, Challenge.lean) == match
assert independent_kernel_check(project) == OK          # e.g., nanoda
return "formally trustworthy; semantic faithfulness rests on step one's human judgment"

• human_review: manually checking that the formal statement matches the paper's statement.
• axioms(...): the set of axioms the proof depends on; any sorry (a placeholder for an unfinished proof) or custom axiom disqualifies it.
• comparator: confirms the proved theorem exactly matches the statement given in advance.

Worked example: If a project quietly added an extra hypothesis "n ≥ 10¹⁰⁰" to its main theorem, the kernel check, axiom audit, and independent kernel would all pass; only step one — "is the statement file equivalent to the paper?" — could catch it. A MechAlign case is exactly this kind: for a result related to hyperbolic groups, it used dependency checks to locate a dimension constraint missing relative to the original manuscript (consistent with the formalization scope declared upstream) [6].

Why it works, and when it fails: Machine checking reduces the uncertainty in "is the proof correct" to a very low level, but concentrates all remaining risk in "is the statement faithful." Axiom's experience illustrates this too: its team repeatedly faced the hard judgment of "does adding a hypothesis merely postpone work, or does it change what the theorem means?", and review had to compare "the proved statement" with "the target statement" [4].

5. Mechanism ③: SemantEq — When Are Two Formal Statements "Truly Equivalent"?

One-line intuition: A common way to check whether a formal statement P is faithful is to prove it equivalent to a trusted reference statement Q (P ↔ Q). But if both P and Q are provable from the library, P ↔ True ↔ Q holds "trivially," and the stronger the prover, the more unrelated pairs get misjudged as equivalent [5].

Analogy: To decide whether two translations say the same thing, you cannot argue "both are true sentences" — "the Earth is round" and "water boils at 100 degrees" are both true, but they are not translations of the same sentence.

Step by step (2026-10-23):

1. Instead of merely requiring "a proof of P ↔ Q exists," require that P can be transformed into Q only through a sequence of permitted steps, such as logical rearrangement or rewriting with the library's own equations.
2. Judge by the proof term that Lean actually checks, not by the surface tactic script, to prevent "detours."
3. Provide a model-free searcher, SemantEq-Eval, and an audit-oriented ProofAudit.

Key formulas:

Trivial equivalence: ⊢ P and ⊢ Q  ⇒  ⊢ P ↔ Q        (content-independent; must be excluded)
SemantEq: P = S₀ → S₁ → … → S_k = Q, each step S_i → S_{i+1} ∈ allowed step set A

• ⊢ P: P is provable in the library; S_i: intermediate statements; A: the set of allowed transformations (logical rearrangement, rewriting with library equations, etc.).

Worked example (illustrative): P is "for all natural numbers n, n + 0 = n," and Q is "2 is prime." Both are provable in the library, so P ↔ Q holds trivially, but they are obviously not two ways of writing the same statement — the transformation chain SemantEq requires does not exist, so they are judged not equivalent. Conversely, P′ is "∀x, ¬(x > 3)" and Q′ is "∀x, x ≤ 3"; a single rewrite with the library equation "not greater than means less than or equal to" turns one into the other, so they are judged equivalent.

Results (per the paper): On the ProofNetVerif test set (labels adjudicated by the authors), SemantEq-Eval achieves 100% precision and 65.6% recall, versus 95.8% and 61.8% for the BEq+ baseline, at the cost of 8.9× more CPU time; ProofAudit misjudges none of 104 non-equivalent pairs as equivalent and raises recall from 65.4% to 81.1% [5].

Why it works, and when it fails: It tightens "equivalence" from "logically inter-derivable" to "structurally inter-transformable," trading some recall for zero false positives. It fails where it needs a trusted reference statement, which often does not exist for brand-new research results; there, project-level review such as MechAlign is needed [6] — it reviewed 201 main results from 173 OpenAI Math projects and built LeanReviewBench, with 501 "claim–statement–context" triples.

6. Mechanism ④: Maestro — On Failure, "Explain Why," and Let a Global Coordinator Decide

One-line intuition: A traditional divide-and-conquer prover facing a lemma it cannot prove just keeps splitting it; but a lemma may resist proof because hints are insufficient, because the lemma is false, or because the higher-level decomposition went wrong. Maestro has provers report "why they failed," and a coordinator that sees the whole picture chooses the response [7].

Analogy: A project manager cannot just hear "this part can't be finished"; they need to know whether it is "missing information," "the requirement itself is contradictory," or "the approach was wrong from the start" — the responses are completely different.

Step by step (2026-10-19):

1. The coordinator decomposes the target theorem into a proof tree and dispatches it to several local provers.
2. Each local prover may modify only its own proof file and may not add declarations such as axioms; when it cannot finish, it returns a structured failure diagnosis with mathematical evidence.
3. Based on the diagnosis, the coordinator chooses a response: guide (give the stuck prover more hints), correct (the lemma is found false; modify the statement), or retract and replan (the whole subtree went the wrong way; roll back and re-decompose).
4. In code synthesis, checked counterexamples send code back for repair.

Pseudocode:

while not proved(root) and budget > 0:
for node in open_leaves(tree):
result = prover(node)               # returns success / failure diagnosis
if result.failed:
match diagnose(result):
"needs guidance"  -> guide(node, hints)
"lemma is false"  -> correct_statement(node)
"bad split"       -> retract(subtree(node)); replan(parent(node))

Worked example (illustrative): To prove A, the plan splits it into lemmas B and C. C fails repeatedly, and the prover reports "counterexample found: C does not hold when x = 0." A traditional system would keep splitting C into C1 and C2, wasting budget; Maestro's coordinator judges "the lemma is false," changes C to "holds when x ≠ 0," and adds a lemma D to handle x = 0.

Results (per the paper): 34/48 proved on arXivLean versus 19 for the baseline; PutnamBench 669/672; Lean-IMO 59/60; IMO 2026 problems 6/6 [7].

Why it works, and when it fails: It turns "failure" into information, avoiding spending the budget in the wrong direction. Its limitation is that the coordinator's own judgment may be wrong — misjudging a "hard but true" lemma as false and modifying the statement — which brings us back to statement faithfulness and requires human oversight.

7. From Tools to Workflows: Human-in-the-Loop Formalization

Several works show formalization evolving from "a prover" into "a workflow":

• Numina Fuse (2026-10-24) [8]: an agent-native application for Lean 4. The authors point out that Lean code can compile without expressing the intended informal meaning, and that agents now write Lean faster than humans can read it, so the system is designed around "humans supervising agents," offering blueprints, dependency graphs, and code views; the paper reports its use in formalizing the three-dimensional Kakeya conjecture.
• PaperFormalizer (2026-10-22) [9]: starting from a paper's LaTeX source, it converts the paper into a statement-dependency graph, reviews each statement for faithfulness, ambiguity, and correctness, and then formalizes it in Lean. Any decision that could change the paper's claims is referred to the authors themselves.
• MechAlign (2026-10-26) [6]: for cases with no trusted reference statement, its extraction tool LeanTrace builds a "statement dependency graph" from elaborated declarations, retaining definition bodies and structure constraints, excluding proof bodies, and stopping at an explicit library boundary; a reviewer model then uses this context to judge whether the main theorem faithfully expresses the manuscript's claim and reports discrepancies with localized evidence. The authors used it for a preliminary review of 201 main results from 173 OpenAI Math projects, and built LeanReviewBench from OpenAI Math, Fermat's Last Theorem, and Kakeya material. Its significance: statement faithfulness must be understood through the whole project's dependencies, since the meaning of a single symbol in the main theorem may be determined by definitions dozens of files away.
• ReuF2F (2026-10-19) [12]: collects 244 formalized open problems from undergraduate research projects as a held-out evaluation that is "not widely studied and hard to leak"; per the paper, the best model solves about 40%.
• Verified program optimization (2026-10-20) [10]: has agents write faster implementations together with machine-checked proofs that they are equivalent to the original — the original implementation is itself the specification, sidestepping the bottleneck of "writing specs." Per the paper, of 189 reference implementations in Verina, proven-faster versions were produced for 156.
• Agentic algorithm design (2026-10-26) [13]: agents propose evolutionary algorithms, use Lean guards to filter out flawed designs, and then prove expected-runtime upper bounds, with no empirical comparison at all; per the paper, with frontier models, 12 of 15 runs across 8 problem classes completed the full pipeline with a machine-checked expected-runtime bound, while the two open-weight models tested did not complete it.

8. Side-by-Side Comparison

9. Our Views

First, "machine-checkable" is becoming the entry ticket for AI scientific results — but not the finish line. OpenAI, Anthropic, and Axiom all make Lean formalization a precondition of release. Yet one sentence in Anthropic's repository puts it most clearly: no machine checks whether the statement file matches the paper [2]. We believe that for some time to come, "statement-faithfulness review" will become a new step alongside peer review.

Second, discovery, verification, and explanation are separating into three distinct contributions. Papex's analysis points out that the model makes the claim, Lean and experts verify it, and human scholars turn lengthy proofs into understandable knowledge — each with different authors, dates, and evidence [3]. This places new demands on authorship, timestamps, and archival infrastructure.

Third, formalization's value lies not only in "proving new theorems" but also in "auditing old knowledge." The CFSG formalization found 34 notable discrepancies [4], including counterexamples that required rewriting proof routes. This suggests that any complex body of knowledge long reliant on "expert consensus" may hide undiscovered gaps.

Fourth, communication about "AI breakthroughs" must be restrained. The ETH refutation is theoretically significant but has almost no direct engineering impact; the Yang–Mills result concerns existence, not the mass gap. Accurately stating "what was proved and what was not" is a basic responsibility of science communication.

10. Outlook

6–12 months:

• The public review of the ETH result will reach preliminary conclusions; whatever the outcome, the review process itself will become a reference model for releasing AI scientific results.
• Statement-faithfulness tools (such as SemantEq and MechAlign) and human-in-the-loop formalization workflows (such as Fuse and PaperFormalizer) will be adopted as submission aids by more mathematics journals and conferences.
• More "known but lengthy" theorems will be fully formalized, with accompanying errata lists.

1–3 years:

• Formal verification may spread from mathematics to more domains "with specifications to follow": algorithm correctness, equivalence of program optimizations [10], and protocol and contract logic.
• Research publishing may adopt a "three-piece" standard: natural-language manuscript + formal proof + statement-alignment report, with independent timestamps and records of model use.
• The risk is a "verification gap": AI output far outpaces human review, and if statement review cannot keep up, formalization may create an illusion of "apparently verified."

11. Implications for Financial Risk Management and Enterprise Deployment

1. Apply the idea of "statement faithfulness" to rule and model validation. Whether the system implementation of risk rules and credit-limit strategies matches the policy documents is, in essence, a question of statement faithfulness. Borrow Anthropic's approach: write core rules as short "specification files" humans can check, then verify the implementation against the specification.
2. Introduce verifiable equivalence checks for critical computations. For performance optimizations in modules such as risk measurement, pricing, and credit-limit calculation, follow the idea of "verified optimization" [10]: the optimized implementation must be equivalent to the original, not merely pass tests.
3. Set up a "failure reason" reporting mechanism. Maestro's lesson applies to model development too: when a model underperforms, distinguish "insufficient data," "wrong assumptions," and "wrong direction" — each calls for a different response.
4. Treat "AI breakthrough" news with caution. When setting technology roadmaps, distinguish theoretical progress from engineering usability.

In building rule engines and scorecards, Hongxi AI has always stressed "clear specifications, verifiable implementations, explainable conclusions." This concentrated showing of formal methods in mathematics further confirms the value of that direction.

12. Conclusion

These late-October events mark AI's move in mathematics from "solving problems" to "delivering machine-checkable research results." But machine checking only answers "is the proof correct"; "is it a proof of the statement we care about" still needs humans to answer. For both the research community and enterprises, the key capability in the next stage is to institutionalize "writing specifications clearly, making them understandable, and making them independently checkable."

Visit Hongxi AI at https://www.hxallai.com.

References

1. [1] OpenAI. Working with academic communities to build scientific understanding. OpenAI, 2026-10-26. https://openai.com/index/building-scientific-understanding-with-academic-communities
2. [2] Anthropic. anthropics/formal-math: the eth project (A 2^o(n) Time Algorithm for 3-SAT — paper and Lean 4 formalization). GitHub, 2026-10-27. https://github.com/anthropics/formal-math
3. [3] Papex. OpenAI's Kakeya, ETH and Yang–Mills claims: what they say and what stays open. Papex Blog, 2026-10-27. (Third-party analysis.) https://papex.org/blog/claimed-verified-explained
4. [4] Axiom. Formalizing the Enormous Theorem. Axiom Math, 2026-10-26. https://axiommath.ai/research/the-enormous-theorem-formalized/
5. [5] Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat, Rianna Jamdar, et al. SemantEq: Faithful Bidirectional Equivalence of Formal Statements. arXiv, 2026-10-23. https://arxiv.org/abs/2610.32919
6. [6] Hao Shen, Ruichen Qiu, Lihong Zhi, Xiao-Shan Gao. MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization. arXiv, 2026-10-26. https://arxiv.org/abs/2610.35269
7. [7] Haoyu Li, Zeren Shui, Yuhao Zhang, Ferhat Erata, et al. Maestro: Agentic Formal Proof Development by Coordination. arXiv, 2026-10-19. https://arxiv.org/abs/2610.25920
8. [8] Justin Asher, Yichuan Cao, Ruichen Qiu, Pietro Pellegrino, et al. Numina Fuse: Interactive Autoformalization in Lean 4. Project Numina, 2026-10-24. https://arxiv.org/abs/2610.33860
9. [9] Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet. PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean. arXiv, 2026-10-22. https://arxiv.org/abs/2610.31810
10. [10] Zhe Ye, Udaya Ghai, Zhizhen Qin, Dawn Song, et al. Agentic Verified Optimization of Real-World Software. arXiv, 2026-10-20. https://arxiv.org/abs/2610.30188
11. [11] Lorenzo Bresolin, Marcello Mamino. Reflections on Trusting Lean. arXiv, 2026-10-21. https://arxiv.org/abs/2610.30433
12. [12] Zeyu Zheng, Yiyang Liu, Yuyang Zhao, Congmin Zheng, et al. ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems. arXiv, 2026-10-19. https://arxiv.org/abs/2610.27046
13. [13] Per Kristian Lehre. Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in Lean. arXiv, 2026-10-26. https://arxiv.org/abs/2610.35595

Research · Frontier AI Deep Dive · Great Unicorn Intelligence