Connect and check the mathprompt Lean specification in CI

[sudoantonio]

Objective

Turn formal/lean_semantic_spec.lean from a research snapshot into a checked
extension of mathprompt.

Acceptance criteria

• The repository declares a reproducible Lean toolchain and dependency on mathprompt.
• Placeholder propositions are identified and replaced incrementally by statements.
• Python structures have a documented mapping to Lean definitions.
• CI compiles the formal project and reports remaining assumptions explicitly.