📝 SummarXiv

Abstract

We present Generative Logic (GL), a deterministic architecture that starts from user-supplied axiomatic definitions (and, optionally, a list of simple facts for counterexample (CE) construction), written in a minimalist Mathematical Programming Language (MPL), and systematically explores their deductive neighborhood. Definitions are compiled into a distributed grid of simple Logic Blocks (LBs) that exchange messages; whenever the premises of an inference rule unify, a new fact is emitted with full provenance to its sources, yielding replayable, auditable proof graphs. A prototype software implementation instantiates the workflow on first-order Peano arithmetic. Starting only from the Peano axioms, GL enumerates conjectures, applies normalization, type, and CE filter, and automatically reconstructs machine-checkable proofs of foundational arithmetic laws, including associativity and commutativity of addition, associativity and commutativity of multiplication, and distributivity. On commodity hardware, the prover phase requires approximately 7 seconds; a complete run finishes in about 5 minutes. Generated proofs export to navigable HTML so that every inference step can be inspected independently. We outline a hardware-software co-design path toward massively parallel realizations and describe prospective integration with probabilistic models (e.g., large language models) for auto-formalization and conjecture seeding. The Python, C++, and MPL code to reproduce the Peano experiments, along with the full proof graphs in HTML as well as machine-readable text format, are available in the project's GitHub repository at github.com/Generative-Logic/GL commit 56c9233 and are permanently archived at doi:10.5281/zenodo.17206386.