feat(provers): implement complete Lean 4 backend

Implements full Lean 4 prover backend with:

Core structures:
- LeanExpr: Expression representation (App, Lambda, Pi, etc.)
- LeanLevel: Universe level representation
- LeanDeclaration: Definitions, theorems, axioms

Parsing (nom combinators):
- Complete Lean 4 syntax parser
- Support for unicode operators and identifiers
- Expression, declaration, and tactic parsing

Tactic application:
- rfl, simp, assumption, intro, apply, rw
- constructor, left, right, decide, ring, omega
- Custom tactics via Tactic::Custom

Verification:
- Lake-based verification pipeline
- temp file generation with proper Lean 4 project structure
- Error parsing and reporting

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Author: Jonathan D.A. Jewell