Skip to content

v1.0.0: Formal verification that u4 is not a single axiom

Choose a tag to compare

View all tags
@fitelson fitelson released this 12 Mar 03:50
· 6 commits to master since this release
v1.0.0
c63d34c

Lean 4 formal verification (zero sorry, no Mathlib dependency) that Ulrich's candidate u4 is not a single axiom for positive implication.

Main result: thm5_not_unifiable — For all i ≥ 1, j ≥ 0, CD(T_i, T_j) is undefined.

Corollary: p → p is not derivable from u4, so Meredith's 17-symbol axiom is the shortest single axiom for positive implication.

Requires Lean 4.28.0-rc1. Build with lake build.

Assets 2
Loading