K-Lean: Lean 4 for Biology (inspired by HEPLean/physlib)

[Heime-Jorgen]

K-Lean: Lean 4 for Biology (inspired by HepLean)

Hi! We built K-Lean inspired by HepLean's approach of applying Lean 4 to a scientific domain.

K-Lean formalizes computational biology: https://github.com/Heime-Jorgen/kenosian-lean4

64 sorry-free contracts covering:

• Enzyme kinetics (Michaelis-Menten, Hill equation, Competitive inhibition)
• Protein structure (AlphaFold RMSD, TM-score, FRET efficiency, Contact probability)
• Longevity science (Gompertz mortality, Weibull survival, Telomere attrition)
• Clinical medicine (eGFR/CKD-EPI, MELD score, Henderson-Hasselbalch)
• Biophysics (Beer-Lambert, Einstein-Stokes, Poiseuille flow, Osmotic pressure)
• Synthetic biology (SynNotch AND-gate, Riboswitch)

HepLean showed that Lean 4 can be applied seriously to a scientific domain. We are doing the same for biology.

Would love to connect with the HepLean team on lessons learned — proof style conventions, Mathlib integration patterns, community building for domain-specific Lean libraries.

[jstoobysmith]

Thanks for this - might be worth posting on the Lean zulip (https://leanprover.zulipchat.com)!

[Heime-Jorgen]

Thanks for the pointer — will post on the Lean Zulip. The Biology stream there (or a new thread in the general/Mathlib channels) seems like the right venue to surface this to a broader Lean audience.

If the physlib maintainers would find it useful to compare notes on Mathlib integration patterns and proof style conventions for domain-specific libraries, we would be glad to connect there as well. K-Lean covers different ground (biology vs physics) but the structural problems — how to handle floating-point vs real-number proofs, how to scope sorry-free coverage — overlap considerably.