How do I run the Lean 4 formalizations?

[igor-kan]

The formal_physics/ and formal_statistics/ projects need Mathlib. What is the recommended way to build them?

[beojun]

Run formal_physics/scripts/verify.sh (or formal_statistics/scripts/verify.sh). It fetches the prebuilt Mathlib oleans with lake exe cache get, then lake builds the library; the first run downloads several GB, later builds are fast. To build offline, replace the [[require]] block in lakefile.toml with a path dependency on a local Mathlib.