2 papers
cs.LO2026
Generating Theorems by Generating Proof Structures (Extended Version)
Christoph Wernhard
We address generating theorems from a given set of axioms, without proof goal, aiming at value from a mathematical point of view or as lemmas for automated proving. As benchmark, w…
cs.LO2025
Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Christoph Wernhard, Zsolt Zombori
Viewing formal mathematical proofs as logical terms provides a powerful and elegant basis for analyzing how human experts tend to structure proofs and how proofs can be structured…