Generative Logic: A Deterministic Reasoning Engine

Nikolai Sergeev

cs.LOJul 25, 2025

Generative Logic: A Deterministic Reasoning Engine

Authors: Nikolai Sergeev

Organizations: Generative Logic UG, Germany

Abstract

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\land 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\implies 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.

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 171 papers

ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning
Apr 7, 2026Kranthi Kommuru, Kunal Khanvilkar, Gaurav ParekhLarge Language Model-Guided Theorem Proving Automated Theorem Proving
Automatic Data Processing, Inc Atlanta, USA · Amazon Web Services, Inc Banglore, India
Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement
Jun 4, 2026Jui-Hui Chung, Ziyang Cai, Zihao Li +14Automated Theorem Proving Lean Theorem Proving
1Princeton Language and Intelligence, Princeton University · 2Amazon.
Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics
Jun 16, 2026Xiyu Zhai, Xinyi Chen, Yiping Wang +3Automated Theorem Proving Dependent Type Theory
University of Washington · University of Innsbruck

Apr 7, 2026J/K move · Enter open · S save

ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning

Kranthi Kommuru, Kunal Khanvilkar, Gaurav Parekh

Automatic Data Processing, Inc Atlanta, USA · Amazon Web Services, Inc Banglore, India

Large Language Model-Guided Theorem Proving Automated Theorem Proving LLM Mathematical Reasoning Reasoning Verification Formal Verification

Open paper AskPDF arXiv

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.

Abstract

Automated Theorem Proving

Explore similar work

ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning

Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement

Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics