Lean 4 Integration ​

The GILC corpus utilizes Lean 4 as its formal verification language.

Architecture ​

Every theorem defined in the Theorem Registry corresponds to a unique .lean module.

text
GILC-Formal/
├── LeanProject/
│   ├── ObserverBoundary.lean
│   ├── ScaleFreeTopology.lean
│   └── FabriconTensor.lean

Compilation Status ​

The local compile status is polled by the CKE (Corpus Knowledge Engine) and exposed to the Verification Dashboard.