Mathematics · proofs · software

Machine-Native Reasoning · Lean sources

Machine Native Reasoning

Declared contract recorded Coverage and evidence

The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

The accepted project pins Lean 4.34.0-rc2. The browser checker uses Lean 4.33.0 as a separate experiment, with some required imports unavailable. Reproduce the recorded environment with the retained compiler and dependency instructions. Retained runtime and replay instructions.

This inspector contains the current MachineTheory root import and its 78 mathematical modules. Historical sources and recorded checks keep their own provenance in the retained package.

Source files 79

Source locations and editions

Files are shown relative to ./.

Historical editions keep their original paths. Package caches and build files are omitted.

79 files