Lean Chemical Theories

This web page is a collection of lean documentation, with a semi-interactive viewer, for the paper Formalizing Chemical Theory using the Lean Theorem Prover by ATOMS Lab at the University of Maryland Baltimore County.

GitHub repository

We have a static branch of our repository where all the proofs are in the state as it was on 2023/06/22, to align with the code referenced in the paper. It compiles with Lean version 3.51.1 and mathlib commit `f2ad3645af9effcdb587637dc28a6074edc813f9` and has been reproduced on both Windows and MacOS operating systems.

The codes will likely evolve to keep up with updates to Lean and mathlib versions. The most up-to-date version can be found in the main branch which is also deployed on this website.

On the left menu, the "General" section provide links with extra information about mathlib and Lean. The "Library" section contains dropdown subsections according to mathlib's tree structure.

The instructions to install Lean, mathlib, and supporting tools are on the official Lean 3 community website which has been archived and is currently being deprecated.