Propositional Logic Combinators: Machine-Verified Proofs in the Platonic Kernel
Mathematics verified. Core theorems are machine-checked in Lean 4.
Prose and presentation may not have been human-reviewed.
Abstract
We present a collection of formally verified theorems in propositional logic, proved in the Platonic proof kernel and exported to Lean 4. The theorems include fundamental combinators (identity, weakening, syllogism, flip, S-combinator, compose3, diamond) and the classical Peirce's law. All proofs achieve Level 3 kernel verification with complete Lean 4 export capability. The verified count is 15, with 9 theorems covering the core propositional combinators.
Length
1,319 words
Claims
9 theorems
Status
paper_and_proof