All life = autocatalyst (cat + mol that cr cat) -> molecular-robot-selfreplicator -> ... -> universal explainer. We can live ∞ (but iff Open Soc of Karl Popper)
-
clean Public
Forked from Certora/cleanC-to-Lean framework based on CompCert
Rocq Prover Other UpdatedOct 10, 2026 -
leancompcert Public
Forked from gersh/leancompcertExperimental Lean-to-CompCert pipeline with verified decision procedures and explicit assurance boundaries
Lean UpdatedOct 9, 2026 -
-
-
Lean Updated
Oct 8, 2026 -
-
-
lean4 Public
Forked from leanprover/lean4Lean 4 programming language and theorem prover
Lean Apache License 2.0 UpdatedOct 7, 2026 -
-
-
-
-
-
-
-
Lean Updated
Oct 1, 2026 -
leanos Public
Forked from rudi-cilibrasi/leanosexperimental LeanOS formally verified OS
Lean Apache License 2.0 UpdatedSep 30, 2026 -
vscode-lean4 Public
Forked from leanprover/vscode-lean4VS Code extension for the Lean 4 programming language and theorem prover
TypeScript Apache License 2.0 UpdatedSep 30, 2026 -
-
systems-lean Public
Forked from SurmountSystems/systems-leanFreestanding high assurance Lean 4 implemented with no runtime GC and linear type multiplicities, compiles AOT to CompCert C
Lean Other UpdatedSep 26, 2026 -
-
-
SciLean Public
Forked from lecopivo/SciLeanScientific computing in Lean 4
Lean Apache License 2.0 UpdatedSep 20, 2026 -
LeanBLAS Public
Forked from lecopivo/LeanBLASBindings and specification for BLAS
Lean Apache License 2.0 UpdatedSep 20, 2026 -
-
-
-
-
-
Previous Next