Lean Kernel Arena / con-leche

Checker "con-leche"

Version: 0d2f467 · 📄 Declaration · 🔗 Source

con-leche is an external Lean checker with a consistency proof: if it accepts a set of declarations, then they have a model in set theory (ZFC with enough inaccessibles) — one set per constant under which every constant is a member of its type — and in particular no theorem of False is accepted. The proof is done directly against a set-theoretic model, not against an abstract typing relation.

Written in Lean, entirely by Claude under close human guidance. It runs in verified mode here (the mode the theorem is about) with four worker threads for the check phase. It accepts only the three standard axioms and declines streams that use others.

Soundness (rightfully rejected tests)

77 ✅ 0 ❌ 3 🚫

Completeness (rightfully accepted tests)

132 ✅ 0 ❌ 6 🚫

Corner cases (no outcome prescribed)

30 ✅ 0 🚫

Test Expected Result ⏱️ 🧠
cedar 👍 🚫 15.0 s 862.9 MB
con-leche 👍 👍 1.83 min (0%) 676.9 MB (-21%)
cslib 👍 👍 6.88 min (-20%) 2.0 GB (-42%)
init 👍 👍 71.4 s (+8%) 537.5 MB (-5%)
init-prelude 👍 👍 378 ms (+4%) 53.4 MB (-27%)
mathlib 👍 👍 21.7 min (-33%) 5.1 GB (-48%)
navier-stokes-euler 👍 👍 7.60 min (-32%) 1.4 GB (-43%)
reachability 👍 👍 31.6 s (+34%) 4.4 GB (×2.7)
std 👍 👍 1.87 min (0%) 732.1 MB (-21%)
26 166 ms 35.4 MB
closure-level-subst ✋ ✋ 4.03 ms 20.7 MB
constlevels ✋ ✋ 4.33 ms 23.0 MB
ctor-num-fields ✋ ✋ 3.72 ms 20.2 MB
eta-ctor-alias ✋ ✋ 4.02 ms 21.2 MB
forged-quot-ind ✋ ✋ 3.78 ms 21.0 MB
k-rec-conv ✋ ✋ 4.33 ms 21.3 MB
large-elim-param ✋ ✋ 3.97 ms 21.1 MB
large-elim-prop-bool ✋ ✋ 4.20 ms 20.8 MB
level-imax-leq ✋ ✋ 3.30 ms 19.9 MB
level-imax-normalization ✋ ✋ 3.96 ms 21.1 MB
loose-bvar-value ✋ ✋ 3.81 ms 20.8 MB
nat-rec-k-lie ✋ ✋ 3.31 ms 20.3 MB
nat-rec-rules ✋ ✋ 3.34 ms 20.1 MB
nested-name-capture ✋ ✋ 5.59 ms 20.8 MB
nested-rec-rule-nfields ✋ ✋ 5.98 ms 22.8 MB
nested-unused-param ✋ ✋ 6.14 ms 21.1 MB
orphan-rec ✋ ✋ 3.22 ms 17.7 MB
pi-closure-context ✋ ✋ 3.88 ms 20.6 MB
proj-non-structure ✋ ✋ 4.06 ms 20.8 MB
proj-of-imax-prop ✋ ✋ 4.58 ms 22.9 MB
proj-of-stuck-prop ✋ ✋ 14.2 ms 33.3 MB
proj-of-subst-prop ✋ ✋ 22.8 ms 33.3 MB
rec-k-lie ✋ ✋ 3.27 ms 19.8 MB
rec-missing-ih ✋ ✋ 14.9 ms 35.4 MB
rec-of-subst-prop ✋ ✋ 23.3 ms 35.0 MB
unit-rec-rule ✋ ✋ 3.98 ms 21.0 MB
1 157 ms 23.2 MB
alg-conv-trans-acc 🤷 ✋ 9.03 ms 23.1 MB
alg-conv-trans-acc-left 🤷 👍 9.05 ms 22.8 MB
alg-conv-trans-acc-right 🤷 👍 9.18 ms 22.9 MB
alg-conv-trans-quot 🤷 ✋ 4.00 ms 21.2 MB
alg-conv-trans-quot-left 🤷 ✋ 4.03 ms 20.8 MB
alg-conv-trans-quot-left-def 🤷 👍 4.10 ms 20.9 MB
alg-conv-trans-quot-right 🤷 👍 4.03 ms 21.2 MB
eta-ctor 🤷 ✋ 4.15 ms 20.8 MB
eta-rec-struct 🤷 ✋ 4.16 ms 21.1 MB
eta-rule-k 🤷 ✋ 3.91 ms 20.7 MB
eta-struct-major-and 🤷 👍 4.09 ms 21.2 MB
eta-struct-major-and-no-whnf 🤷 👍 4.87 ms 20.8 MB
eta-struct-major-no-whnf 🤷 👍 5.68 ms 23.0 MB
eta-unit-like-nested 🤷 ✋ 4.55 ms 21.0 MB
eta-unit-like-pi 🤷 ✋ 3.97 ms 21.0 MB
eta-unit-like-proof-field 🤷 ✋ 4.07 ms 21.0 MB
eta-unit-like-struct 🤷 ✋ 4.08 ms 21.3 MB
imax-nested-absorption 🤷 👍 3.83 ms 20.8 MB
imax-right-successor 🤷 👍 3.79 ms 20.8 MB
large-elim-maybe-prop 🤷 👍 3.97 ms 21.1 MB
let-value-type-mismatch 🤷 ✋ 3.78 ms 21.1 MB
nested-nonuniform-param 🤷 ✋ 4.16 ms 20.8 MB
nested-redex-aux 🤷 👍 7.35 ms 23.1 MB
positivity-whnf 🤷 ✋ 3.95 ms 21.0 MB
proj-maybe-prop 🤷 👍 4.21 ms 21.1 MB
proj-maybe-prop-past 🤷 👍 4.21 ms 20.9 MB
proof-param-ok 👍 👍 3.98 ms 20.8 MB
proof-param-swap 🤷 ✋ 3.83 ms 20.7 MB
subject-reduction-redex 🤷 ✋ 9.27 ms 23.2 MB
subject-reduction-reduct 🤷 ✋ 9.12 ms 22.8 MB
vanishing-occurrence 🤷 👍 4.20 ms 21.1 MB
8 43.3 ms 23.1 MB
extra-rec ✋ ✋ 3.22 ms 18.2 MB
inductive-undeclared-universe ✋ ✋ 3.82 ms 21.1 MB
level-index-out-of-order 👍 🚫 3.77 ms 22.4 MB
nat-lit-add 👍 👍 5.30 ms 23.1 MB
nat-lit-add-bad ✋ ✋ 5.28 ms 22.5 MB
nat-lit-ble 👍 👍 5.40 ms 20.8 MB
nat-lit-sub 👍 👍 5.57 ms 23.1 MB
orphan-ctor ✋ ✋ 3.22 ms 20.2 MB
proj-of-prop ✋ ✋ 4.01 ms 20.8 MB
sparse-name-index 👍 🚫 3.76 ms 20.7 MB
31 1.88 min (+40%) 7.3 GB
app-lam 👍 👍 4.08 s (-16%) 1.2 GB (-12%)
args-before-unfold 👍 👍 14.4 ms (÷2.5) 23.8 MB (÷2.8)
beta-ladder 👍 👍 906 ms (-46%) 396.3 MB (-21%)
church-numerals 👍 👍 53.7 ms (+14%) 46.0 MB (-41%)
discarded-argument 👍 👍 12.8 ms (÷13) 23.2 MB (÷2.8)
discarded-argument-match 👍 👍 36.9 ms (÷3.9) 24.9 MB (÷2.7)
folded-constant-first 👍 👍 19.8 ms (÷2.1) 24.4 MB (÷2.8)
folded-constant-last 👍 👍 19.7 ms (÷2.1) 24.4 MB (÷2.8)
fueled-chain 👍 👍 70.7 ms (-44%) 45.5 MB (-40%)
grind-ring-5 👍 👍 2.95 s (+37%) 201.2 MB (-12%)
identical-nesting 👍 👍 4.20 ms (÷6.7) 22.9 MB (÷2.9)
irrelevance-before-evaluation 👍 👍 4.70 ms (÷6.1) 21.1 MB (÷3.1)
irrelevance-refutes 👍 👍 4.35 ms (÷6.6) 21.1 MB (÷3.1)
let-fold 👍 👍 2.46 s (×42) 351.5 MB (×5.3)
let-ladder 👍 👍 487 ms (÷2.1) 225.5 MB (-29%)
magma-list-deep-n21 👍 👍 3.93 s (+46%) 595.5 MB (-11%)
magma-list-deep-n36 👍 👍 46.9 s (+32%) 7.3 GB (-6%)
magma-list-pair-n21 👍 👍 31.1 s (+68%) 5.1 GB (+28%)
magma-list-pair-n7 👍 👍 2.81 s (+67%) 475.2 MB (+12%)
magma-string-n4 👍 👍 4.92 s (+39%) 137.9 MB (+14%)
magma-string-pair-n9 👍 👍 11.8 s (+44%) 966.4 MB (-3%)
proj-cheap-struct 👍 👍 9.67 ms (÷3.6) 22.9 MB (÷2.9)
proj-lazy-struct 👍 👍 6.63 ms (÷4.7) 23.0 MB (÷2.9)
proj-stuck-struct 👍 👍 6.94 ms (÷4.6) 22.9 MB (÷2.9)
prop-struct-projections 👍 👍 451 ms (×4.5) 49.6 MB (-29%)
refute-cheap-first ✋ ✋ 4.88 ms (÷8.6) 23.2 MB (÷3.0)
refute-cheap-last ✋ ✋ 15.6 ms (÷12) 22.7 MB (÷3.0)
repeated-subproblem 👍 👍 4.53 ms (÷6.3) 21.1 MB (÷3.1)
shared-subterm 👍 👍 39.3 ms (-32%) 28.1 MB (÷2.6)
shift-cascade 👍 👍 12.8 ms (÷3.6) 33.1 MB (÷2.0)
unroll-versus-evaluate 👍 👍 7.49 ms (÷4.1) 23.6 MB (÷2.8)
135 556 ms 23.3 MB
001_basicDef 👍 👍 3.78 ms 20.8 MB
002_badDef ✋ ✋ 3.77 ms 20.6 MB
003_arrowType 👍 👍 3.78 ms 20.6 MB
004_dependentType 👍 👍 3.79 ms 21.1 MB
005_constType 👍 👍 3.79 ms 20.8 MB
006_betaReduction 👍 👍 3.82 ms 21.0 MB
007_betaReduction2 👍 👍 3.83 ms 20.9 MB
008_forallSortWhnf 👍 👍 3.82 ms 20.8 MB
009_forallSortBad ✋ ✋ 3.82 ms 21.0 MB
010_nonTypeType ✋ ✋ 3.81 ms 20.7 MB
011_nonTypeAxiom ✋ ✋ 3.78 ms 20.9 MB
012_nonPropThm ✋ ✋ 3.79 ms 20.5 MB
013_thmProof 👍 👍 3.82 ms 20.6 MB
014_selfProof ✋ ✋ 3.78 ms 20.8 MB
015_levelComp1 👍 👍 3.78 ms 20.9 MB
016_levelComp2 👍 👍 3.78 ms 20.8 MB
017_levelComp3 👍 👍 3.78 ms 20.6 MB
018_levelParams 👍 👍 3.83 ms 20.8 MB
019_tut06_bad01 ✋ ✋ 3.76 ms 20.6 MB
020_levelComp4 👍 👍 3.77 ms 20.5 MB
021_levelComp5 👍 👍 3.79 ms 22.4 MB
022_imax1 👍 👍 3.79 ms 21.1 MB
023_imax2 👍 👍 3.79 ms 20.7 MB
024_levelMaxComm 👍 👍 3.78 ms 20.6 MB
025_levelMaxAssoc 👍 👍 3.80 ms 20.8 MB
026_levelMaxIdem 👍 👍 3.79 ms 20.9 MB
027_levelMaxAbsorb 👍 👍 3.79 ms 20.9 MB
028_inferVar 👍 👍 3.79 ms 20.7 MB
029_defEqLambda 👍 👍 3.82 ms 21.1 MB
030_peano1 👍 👍 3.97 ms 23.1 MB
031_peano2 👍 👍 4.05 ms 20.8 MB
032_peano3 👍 👍 4.13 ms 22.8 MB
033_letType 👍 👍 3.78 ms 21.0 MB
034_letTypeDep 👍 🚫 3.81 ms 20.6 MB
035_letRed 👍 🚫 3.79 ms 20.6 MB
036_empty 👍 👍 3.80 ms 20.6 MB
037_boolType 👍 👍 3.81 ms 22.9 MB
038_twoBool 👍 👍 3.95 ms 20.8 MB
039_andType 👍 👍 3.83 ms 20.9 MB
040_prodType 👍 👍 4.04 ms 23.0 MB
041_pprodType 👍 👍 4.04 ms 21.1 MB
042_pUnitType 👍 👍 3.88 ms 21.2 MB
043_eqType 👍 👍 3.84 ms 20.6 MB
044_natDef 👍 👍 3.96 ms 20.9 MB
045_rbTreeDef 👍 👍 5.53 ms 20.5 MB
046_inductBadNonSort ✋ ✋ 3.78 ms 21.1 MB
047_inductBadNonSort2 ✋ 🚫 3.76 ms 23.1 MB
048_inductLevelParam ✋ ✋ 3.76 ms 20.8 MB
049_inductTooFewParams ✋ ✋ 3.76 ms 20.7 MB
050_inductWrongCtorParams ✋ ✋ 3.23 ms 18.0 MB
051_inductWrongCtorResParams ✋ ✋ 3.24 ms 19.9 MB
052_inductWrongCtorResLevel ✋ ✋ 3.24 ms 18.1 MB
053_inductInIndex ✋ ✋ 3.22 ms 17.8 MB
054_indNeg ✋ ✋ 3.23 ms 18.0 MB
055_reduceCtorParam.mk 👍 👍 4.07 ms 21.1 MB
056_reduceCtorType.mk ✋ ✋ 3.24 ms 18.0 MB
057_indNegReducible ✋ ✋ 3.24 ms 17.9 MB
058_predWithTypeField 👍 👍 3.90 ms 20.8 MB
059_typeWithTypeField 👍 👍 3.92 ms 20.7 MB
060_typeWithTypeFieldPoly 👍 👍 3.91 ms 20.8 MB
061_typeWithTooHighTypeField.mk ✋ ✋ 3.22 ms 17.9 MB
062_emptyRec 👍 👍 3.82 ms 20.7 MB
063_boolRec 👍 👍 3.85 ms 20.8 MB
064_twoBoolRec 👍 👍 3.99 ms 20.9 MB
065_andRec 👍 👍 3.86 ms 20.7 MB
066_prodRec 👍 👍 4.07 ms 20.9 MB
067_pprodRec 👍 👍 4.08 ms 20.8 MB
068_punitRec 👍 👍 3.90 ms 21.0 MB
069_eqRec 👍 👍 3.86 ms 21.0 MB
070_nRec 👍 👍 3.99 ms 21.0 MB
071_rbTreeRef 👍 👍 5.66 ms 20.6 MB
072_boolPropRec 👍 👍 3.92 ms 20.8 MB
073_BogusRecursor ✋ ✋ 3.23 ms 17.9 MB
074_existsRec 👍 👍 4.08 ms 21.3 MB
075_typeSingletonRecReduction 👍 👍 4.02 ms 20.9 MB
076_sortElimPropRec 👍 👍 4.11 ms 20.8 MB
077_sortElimProp2Rec 👍 👍 4.17 ms 20.8 MB
078_boolRecEqns 👍 👍 4.03 ms 21.1 MB
079_prodRecEqns 👍 👍 4.25 ms 21.0 MB
080_nRecReduction 👍 👍 4.30 ms 20.9 MB
081_listRecReduction 👍 👍 4.66 ms 21.0 MB
082_RBTree.id_spec 👍 👍 7.27 ms 23.3 MB
083_And.right 👍 👍 3.87 ms 21.1 MB
084_Prod.snd 👍 👍 4.09 ms 21.2 MB
085_PProd.snd 👍 👍 4.10 ms 20.9 MB
086_PSigma.snd 👍 👍 4.15 ms 21.0 MB
087_projOutOfRange ✋ ✋ 3.83 ms 20.6 MB
088_projNotStruct ✋ ✋ 3.99 ms 20.5 MB
089_projProp1 👍 👍 4.23 ms 21.1 MB
090_projProp2 ✋ ✋ 4.24 ms 21.0 MB
091_projProp3 👍 👍 4.25 ms 21.1 MB
092_projProp4 ✋ ✋ 4.23 ms 20.7 MB
093_projProp5 ✋ ✋ 4.25 ms 20.9 MB
094_projProp6 ✋ ✋ 4.25 ms 21.0 MB
095_projDataIndexRec 👍 👍 4.25 ms 20.7 MB
096_projIndexData ✋ ✋ 4.67 ms 22.9 MB
097_projIndexData2 ✋ ✋ 4.65 ms 20.7 MB
098_projRed 👍 👍 4.19 ms 20.9 MB
099_ruleK 👍 👍 3.91 ms 20.8 MB
100_ruleKbad ✋ ✋ 3.95 ms 21.0 MB
101_ruleKAcc ✋ ✋ 4.50 ms 20.9 MB
102_aNatLit 👍 👍 3.82 ms 20.7 MB
103_natLitEq 👍 👍 3.88 ms 21.1 MB
104_proofIrrelevance 👍 👍 3.89 ms 21.2 MB
105_proofIrrelevanceBad ✋ ✋ 3.90 ms 21.0 MB
106_proofIrrelevanceWhnf 👍 👍 3.94 ms 20.7 MB
107_proofIrrelevanceUnderBinder 👍 🚫 3.84 ms 20.7 MB
108_unitEta1 👍 👍 4.00 ms 21.0 MB
109_unitEta2 👍 👍 3.98 ms 21.3 MB
110_unitEta3 👍 👍 3.97 ms 20.9 MB
111_indexedUnitEta ✋ ✋ 4.02 ms 23.1 MB
112_structEta 👍 👍 4.34 ms 21.1 MB
113_indexedStructEta ✋ ✋ 4.12 ms 21.0 MB
114_funEta 👍 👍 3.92 ms 21.1 MB
115_funEtaDep 👍 👍 3.93 ms 21.0 MB
116_funEtaBad ✋ ✋ 3.90 ms 20.9 MB
117_reflOccLeft ✋ ✋ 3.28 ms 19.8 MB
118_reflOccInIndex ✋ ✋ 3.29 ms 19.9 MB
119_reduceCtorParamRefl.mk 👍 👍 4.11 ms 21.1 MB
120_reduceCtorParamRefl2.mk 👍 👍 4.11 ms 20.6 MB
121_rTreeRec 👍 👍 4.09 ms 23.1 MB
122_rtreeRecReduction 👍 👍 4.25 ms 21.1 MB
123_accRecType 👍 👍 4.40 ms 20.8 MB
124_accRecReduction 👍 👍 4.55 ms 20.9 MB
125_accRecNoEta ✋ ✋ 4.50 ms 20.8 MB
126_quotMkType 👍 👍 3.87 ms 20.9 MB
127_quotIndType 👍 👍 3.90 ms 20.8 MB
128_quotLiftType 👍 👍 3.89 ms 21.1 MB
129_quotSoundType 👍 👍 3.90 ms 20.8 MB
130_quotLiftReduction 👍 👍 3.99 ms 21.1 MB
131_quotIndReduction 👍 👍 3.97 ms 20.8 MB
132_dup_defs ✋ ✋ 3.78 ms 20.9 MB
133_dup_ind_def ✋ ✋ 3.80 ms 21.0 MB
134_dup_ctor_def ✋ ✋ 3.80 ms 20.8 MB
135_dup_rec_def ✋ ✋ 3.83 ms 20.8 MB
136_misnamed_rec_user ✋ ✋ 3.82 ms 20.9 MB
137_dup_rec_def2 ✋ ✋ 3.81 ms 20.5 MB
138_dup_ctor_rec ✋ ✋ 3.82 ms 21.0 MB
139_DupConCon ✋ ✋ 3.23 ms 20.0 MB
140_falseFromUnsafe ✋ 🚫 3.23 ms 17.9 MB
141_falseFromPartial ✋ 🚫 3.22 ms 18.0 MB