We present Generative Logic (GL), a deterministic computer architecture for automated mathematical reasoning. GL starts from axiomatic definitions written in a minimalist Mathematical Programming Language (MPL) and explores a configurable region of their deductive neighborhood. The definitions are compiled into a grid of Logic Blocks (LBs). An LB applies rules by hash-table lookups, and every statement it derives keeps its complete provenance. A run generates conjectures, removes those that counterexamples refute, tries to prove the rest, reduces the proved theorems to an essential core and writes every proof as navigable HTML. An independent verifier checks every proof step. From supplied definitions, GL derives the basic laws of Peano arithmetic and Gauss's summation formula. From previously proved lemmas, further definitions and a supplied list of conjectures, it builds a proof of the Fundamental Theorem of Arithmetic (FTA). These proofs are also exported to Lean 4 and checked by the Lean kernel. The next step is for GL to derive the FTA as well, without supplied conjectures. GL is designed together with a hardware architecture, the Mathematical Processing Unit (MPU).
Figures & tables
Figure 1: The GL pipeline. The MPL definitions feed both the Incubator (step 0) and the main pipeline, and the fact tables of the Incubator feed the CE filter. The configuration files of a batch limit the conjecturer and the depth of the prover. The proof graph is checked by the verifier, written as HTML and exported to Lean 4, where the Lean kernel checks it. A run executes the pipeline in ordered batches.
Figure 2: Two connected LBs. LB 2 receives the statement m>2 from LB 1 by mail. Its hash table holds the key n>m∧m>2 with the value n>2 , so a request from its known statements derives the new statement n>2 .
Figure 3: Mapping the conjecture 0+n=m⟹n+0=m onto a chain of LBs. LB 1 holds the definition of the natural numbers, LB 2 the statement 0+n=m , and the conclusion n+0=m is the goal of LB 2.
Figure 4: Shared tree structure for three conjectures. Conjectures with a common beginning of their premise chains share its LBs: all three share LB A, for example the definition of the natural numbers, and conjectures 1 and 2 also share LB B. The chains branch where the premises differ.
Figure 5: Compiled structure of the fold definition. Existence and and-nodes expand further; implication nodes are terminal; predicate leaves are atomic statements. The Deterministic Logical Transformer traverses the same map in both directions.
Figure 6: A case split in the scope tree of an LB, for the example in the text. The two case scopes open one after the other, each with its disjunct as its assumption. When both reach P(n) , the goal holds in the parent scope and the case scopes are removed.
Figure 7: Overview of the MPU. LB cores with arrays of integer units and an MMU each reach the SRAM blocks through a memory network; mail is a read of the ancestors’ logs. A pager keeps the working set of LB memory in SRAM and moves the rest to an SSD.
Figure 8: The proof index in common notation. Each entry links to its chapter and to its Lean version; “Used by” lists the chapters that cite the theorem.
Figure 9: The proof page of the uniqueness part of the FTA in common notation: two nonincreasing sequences of primes with the same product are equal.
Figure 10: The Lean 4 page of the same proof. Each proof step of the HTML page is one named fact in Lean, and the Lean kernel checks the whole proof.
Batch
Conjecturer
CE filter
Prover
Total
Incubator Peano 1
1.9
—
51.2
59.5
Incubator Peano 2
0.5
—
7.0
8.6
Peano
41.8
4.1
8.4
60.0
Incubator Gauss 1
0.9
—
27.7
34.2
Incubator Gauss 2
0.2
—
6.5
8.4
Incubator Gauss 3
0.3
—
1.4
2.1
Table 1: Run time in seconds by batch on the laptop workstation. The prover column includes the hash bursts, which run on the GPU. Total is the time of the conjecturer and of the batch’s executable, which runs the CE filter, the prover and the compressor. The processing of the proofs, the HTML, the verifier and the Lean export run once per run and are included only in the full-run time. —: the batch has no such stage.
System
Input
Conjectures and filter
Proof
Check of the proof
AM
concepts and heuristics
from examples; interestingness
none
—
Graffiti and successors
objects and invariants
inequalities that hold on all stored objects
by humans
—
HR
concepts and examples, or axioms
from examples; counterexample search
OTTER
none reported
MATHsAiD
axioms and definitions
generated; triviality filters
own prover with induction
none reported
HipSpec, Hipster
functional programs or Isabelle theories
equations; random testing
induction
Hipster: Isabelle’s kernel
TheSy
datatypes and recursive functions
equations; symbolic comparison
own prover with induction
none reported
Table 2: Comparison of GL with discovery systems and provers, as described in the cited sources. “—”: not applicable.
The large language models (LLMs) might produce a persuasive argument within mathematical and logical fields, although such argument often includes some minor missteps, including the entire omission of side conditions, invalid inference patterns, or appeals to a lemma that cannot be derived logically out of the context being discussed. These omissions are infamously hard to notice solely out of the text, as even the misconstrued construction still may seem mostly accurate. Conversely, interactive theorem provers like Lean and Coq have rigorous reliability by ensuring that syntactic and semantic statements only accept statements that can pass all the syntactic and semantic steps in the program which is a small trusted kernel of the language type-checks with. Despite the fact that this technique provides strong guarantees, it comes at quite a heavy price: the evidence must be completely formalized, and the evidence user or a auxiliary search program must provide an avalanche of low-level information. This paper presents a hybrid pipeline where an LLM generates a typed proof sketch in a compact DSL and a lightweight trusted kernel expands the sketch into explicit proof obligations.
Kranthi Kommuru, Kunal Khanvilkar, Gaurav Parekh
Automatic Data Processing, Inc Atlanta, USA · Amazon Web Services, Inc Banglore, India
We introduce Goedel-Architect, an agentic framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement. A blueprint is a dependency graph of definitions and lemmas that builds up to the main theorem. First, Goedel-Architect generates a blueprint of formally stated definitions and lemmas, along with declared dependencies. This blueprint is optionally guided by a natural language proof. Then, a tool-equipped Lean prover component closes each open lemma node in parallel using relevant dependencies. Failed lemmas in turn drive refinement of the global blueprint. This strategy contrasts with other mainstream approaches which use recursive lemma decomposition, and can inefficiently loop on dead-end strategies. Using the open-weight DeepSeek-V4-Flash (284B-A13B) as the backbone, Goedel-Architect attains 99.2% pass@1 on MiniF2F-test and 75.6% pass@1 on PutnamBench. With an optional natural-language proof seeding the initial blueprint on the harder problems, we additionally close the remaining two MiniF2F-test problems (reaching 100%), lift PutnamBench to 88.8% (597/672), and solve 4/6 on IMO 2025, 11/12 on Putnam 2025, and 3/6 on USAMO 2026. This represents state-of-the-art performance for an open-source pipeline at a price point up to 500x less than comparable open-source pipelines.
Jui-Hui Chung, Ziyang Cai, Zihao Li +14
1Princeton Language and Intelligence, Princeton University · 2Amazon.
We present a dependent-type-based prover designed around the way LLMs (and humans) tend to write mathematics, complementing existing systems such as Lean and Rocq. Its core design choices are a surface that imitates mathematical natural language and a rule-driven automation layer that closes the routine steps a textbook would omit, so that an accepted proof can be re-emitted as a checked Lean file. Early experiments suggest that, even without any prover-specific training data, LLMs can learn to use it effectively on the miniF2F benchmark. Lean output excerpts: https://github.com/xiyuzhai-husky-lang/visored/
Xiyu Zhai, Xinyi Chen, Yiping Wang +3
University of Washington · University of Innsbruck