fitelson/u4_lean: Lean 4 formal verification that Ulrich's u4 is not a single axiom for positive implication
Abstract
Add TPTP input and Python verification script; update paper title
Fields of Study & Subjects
Logic
programming
and type systems
Advanced Algebra and Logic
Reasoning
and Knowledge
Publication details
- Journal / source
- Zenodo (CERN European Organization for Nuclear Research)
- Publication date
- 12 March 2026
- Language
- EN