Module lean_gen 

Lean 4 code generator — Phase 7 of the pipeline.

Generates Lean 4 source files from YAML kernel contracts:

• Definition files with kernel functions as Lean def over ℝ
• Theorem stubs with sorry for each proof obligation that has a lean block
• Import structure based on Mathlib dependencies

Also provides lean_status for reporting proof status across contracts.

Structs

LeanFile

A generated Lean 4 file.

LeanStatusReport

Status report for Lean proofs in a single contract.

ObligationStatus

Status of a single obligation’s Lean proof.

Functions

format_status_report

Format a LeanStatusReport as a human-readable table.

generate_lean_files

Generate Lean 4 source files from a contract.

lean_status

Report Lean proof status for a contract.