We introduce the Axiom Engine, a method for systematic knowledge derivation through combinatorial pairing of formal axioms, using a large language model (LLM) as both derivation generator and plausibility filter, with automated formal verification via the Z3 SMT solver. Applied to classical thermodynamics with 8 axioms (the four laws of thermodynamics, the ideal gas law, the Clausius inequality, Carnot efficiency, and the Boltzmann entropy equation), the method exhaustively processed all 28 unique pairwise combinations. Each pair was subjected to a four-step protocol: LLM-generated derivation, self-assessment with novelty and validity scoring, adversarial cross-verification, and classification. Key results: 93% of derivations were rated valid (≥4/5), 54% were classified as genuine insights, and 14% exhibited potentially original formulations. The top 5 derivations and one level-2 result were formally verified with Z3, achieving a 6/6 confirmation rate. Level-2 derivations — combinations of first-level results ("axioms of axioms") — showed 54% higher mean novelty than level-1 (4.33/5 vs. 2.82/5), confirming that iterative derivation amplifies conceptual depth. The most significant result is a level-2 derivation demonstrating that classical thermodynamic axioms, when systematically combined, predict the necessity of non-entropic forces at absolute zero — precisely where quantum mechanics enters historically. The system detected an incompleteness in its own axiom set: it derived a formally correct conclusion (entropic pressure vanishes at T=0) that is empirically insufficient (Fermi degeneracy pressure exists at T=0), thereby identifying the specific boundary where additional axioms are required. This constitutes a primitive form of automated axiomatic incompleteness detection. The work originated during the development of Sigma Vox Pro, an on-device multilingual voice assistant, where a five-layer knowledge indexing architecture (morphological analysis, phonetic recovery, syntactic extraction, intent classification, and structural rejection) embodied the core principle later generalized to axiomatic derivation: separating what a system knows from what it generates. The Axiom Engine demonstrates that LLMs, when constrained by formal axioms and validated by automated theorem provers, can function as structured discovery tools rather than mere text generators.
Mello et al. (Mon,) studied this question.