Prove literal Dedekind formula declaration - #263

Draft

DomTheDeveloper wants to merge 7 commits into

mainfrom

openai/solve-dedekind-literal

Commits on Jul 26, 2026

Prove the literal Dedekind formula question
DomTheDeveloper
committed
aa6a038
Add focused Dedekind Lean audit
DomTheDeveloper
committed
98f713d
Avoid false-positive source scan match
DomTheDeveloper
committed
fa627a2
Expose Dedekind Lean diagnostics
DomTheDeveloper
committed
deeab0c
Upload Dedekind compiler diagnostics
DomTheDeveloper
committed
bb985fd
Build Dedekind module through Lake
DomTheDeveloper
committed
8a1612a
Make the Dedekind literal proof kernel-trivial
DomTheDeveloper
committed
1ae43ff