Translation Explorer

Theorem is open-sourcing a Lean translation of the 1276 theorems in Software Foundations Volume 1, along with proofs that the Lean translation is isomorphic to the original Rocq. This is the first project scaling AI software verification to handle codebases with dependencies. While more compact solutions are possible, our current approach produced ~60k LoC in Lean, proven isomorphic with ~720k LoC of Rocq.

In this explorer, each node corresponds to a theorem statement in Volume 1 of Software Foundations. The different colors represent different modules. Higher color opacities represent nodes with more children, and lower color opacities represent those with less. Clicking on any node will show its direct dependencies and dependents, not including the recursive enumeration.