Automated Theorem Generation in First-Order Logic by Construction from Triangular Standard Contradictions
Authors: Yang Xu, Shuwei Chen, Hailin Guo, Jun Liu
Organizations: School of Mathematics, Southwest Jiaotong University, Chengdu, 611756, China · National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu, 611756, Sichuan, China · School of Computing, Faculty of Computing, Engineering and the Built Environment, Ulster University, Belfast, Northern Ireland, United Kingdom
Automated theorem generation (ATG) seeks to construct new theorems rather than merely prove given conjectures. Existing approaches typically generate candidate statements that require subsequent proof or formal verification. We propose a constructive framework for ATG in first-order logic based on triangular standard contradictions. The method constructs minimally unsatisfiable clause sets from selected first-order literals, then forms theorems by retaining some clauses as premises and taking the negation of one clause, or a conjunction of clauses, as the conclusion. Minimal unsatisfiability ensures that the remaining premises are satisfiable, avoiding trivial inference by explosion, while unsatisfiability of the full set guarantees the resulting entailment. Theorems are therefore correct by construction, without a separate proof procedure for each instance. Extending the previously developed Δ1 generator, we introduce seven methods, Δ2--Δ8, forming a unified family of eight theorem-generation methods. Four generators, Δ1--Δ4, have been implemented and released. We also formulate a general Δ-class method encompassing the family. Combinatorial analysis demonstrates the capacity to generate large numbers of distinct theorems systematically. This framework offers a principled foundation for automated theorem discovery and the construction of logically guaranteed knowledge.
Figures & tables
Figure 1: Schematic representation of a triangular standard contradiction Π(S) . Strictly speaking, the outer shape shown in the figure is a trapezoid; however, since its essential structure is triangular, we follow the established terminology and refer to it as triangular.
Figure 2: A five-column triangular standard-contradiction example. The descending red line connects the generating-literal positions; the horizontal and vertical red segments indicate geometric placement and alignment. The lines do not represent logical operators or additional literals. The literals in each column form the disjuncts of the corresponding clause.
Figure 3: Schematic representation of the full triangular standard contradiction underlying the Δ1 method.
Figure 4: Schematic representation of a Type-I triangular sub-standard contradiction Π(S) used in the Δ2 method. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .
Figure 5: Schematic representation of a Type-II triangular standard contradiction Π(S) used in the Δ3 method. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .
Figure 6: Schematic representation of a Type-III triangular standard contradiction Π(S) used in the Δ4 method. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .
Figure 7: Schematic representation of a Type-IV triangular standard contradiction Π(S) used in the Δ5 method. The sets L1 and L2 represent the two parts of the literals distributed between Cn and Cn+1 , respectively. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .
Figure 8: Schematic representation of a Type- V(i) triangular standard contradiction Π(S(i)) used in the Δ6(i) method, where i∈{n−1,…,2} . The sets L1 and L2 represent the two groups of literals separated at the index i . The hatched region indicates the admissible region for interior literals according to Definition 4.1 .
Figure 9: Schematic representation of a Type- VI(i) triangular standard contradiction Π(S(i)) used in the Δ7(i) method, where i∈{n−1,…,2} . The sets L1=Ci∖{xi} and L2=Cn∖{xn} represent the two groups of complementary literals. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .
Figure 10: Schematic representation of a Type- VII(i) triangular standard contradiction Π(S(i)) used in the Δ8(i) method, where i∈{n−1,…,2} . The sets L3 , L4 , and L5 represent the groups of literals distributed among Cn , Cn+1 , and Ci , respectively. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .
Figure 11: Schematic representation of the general construction of a minimally unsatisfiable clause set from a triangular standard contradiction. The literal y has a predicate symbol that occurs nowhere else in the clause set.
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).
We propose a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures. This design implements the core features shared among state-of-the-art systems: iterative proof refinement, library search and context management. We evaluate this agentic approach using qualitatively different benchmarks and compare various frontier language models and design choices. Our results show competitive performance compared to state-of-the-art approaches, while using a significantly simpler architecture and a fraction of their cost. Additionally, we demonstrate consistent advantages of an iterative approach over multiple single-shot generations, especially in terms of sample efficiency and cost effectiveness. The implementation is released open-source as a candidate reference for future research and as an accessible prover for the community.
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.