Querex | November 2025
Introducing Lean 4 MCP
Mathematical Certification for Your Analytics Pipeline
Transform "I think this is right" into "I can prove this is right."
The Missing Piece in Your Quantitative Workflow
You've been using our MCP tools to build sophisticated analytics pipelines:
Power BI MCP
Extracts real-time data from semantic models
Statistics MCP
Runs hypothesis tests and fits distributions
OR-Tools MCP
Optimizes portfolios, schedules, and allocations
💡 But here's a question that keeps coming up:
"How do I prove these calculations are correct?"
Not test. Not validate. Prove.
Today, we're releasing Lean 4 MCP — and it answers that question definitively.
What is Lean 4?
Lean is a theorem prover used by mathematicians to formally verify proofs. It's the same technology behind recent breakthroughs like the formal verification of the Polynomial Freiman-Ruzsa conjecture.
But you don't need to be a mathematician to use it.
For quantitative finance and analytics, Lean serves as a certified calculator — it can mathematically prove that:
- ✓ Your portfolio weights sum to exactly 100%
- ✓ All constraints from your optimizer are satisfied
- ✓ Your formulas match the Basel/regulatory definitions
- ✓ No copy-paste or unit conversion errors crept in
Lean Catches What Testing Misses
Example 1
Floating Point Accumulation
-- Weights from "optimizer"
def w1 : Float := 0.333333
def w2 : Float := 0.333333
def w3 : Float := 0.333333
#eval w1 + w2 + w3 -- Returns: 0.999999
#eval (w1 + w2 + w3) == 1.0 -- Returns: false ❌Impact: On a $10 billion portfolio, that's $10,000 unallocated.
Example 2
Unit Confusion (15 vs 0.15)
def portfolioValue : Float := 100000000 -- $100M
def volatility_WRONG : Float := 15.0 -- Should be 0.15!
def VaR := portfolioValue * volatility_WRONG * 2.326 * 0.199
#eval VaR -- Returns: $695,000,000 ❌
-- VaR > Portfolio Value = Impossible!Impact: A 15% vs 0.15 mixup creates a 100x error.
Example 3
Constraint Violation
def portfolioPD : Float :=
0.05 * 1.80 + 0.20 * 3.85 + 0.25 * 5.35 +
0.25 * 7.88 + 0.15 * 9.36 + 0.10 * 13.48
#eval portfolioPD -- Returns: 6.92%
#eval portfolioPD ≤ 6.0 -- Returns: false ❌Impact: The "optimal" solution violates your risk constraint.
How It Integrates
Lean MCP slots naturally into your existing workflow:
Data
Tests
Optimize
Price
Verify ✓
Pattern 1: Portfolio Optimization Certification
Power BI → OR-Tools → Lean
- Extract holdings from Power BI
- Optimize allocation with OR-Tools
- Verify all constraints in Lean
Pattern 2: Risk Calculation Audit
Power BI → Quant Finance → Lean
- Get portfolio positions
- Calculate VaR with Quant Finance MCP
- Verify formula implementation in Lean
Available Tools
lean_check
Type-check code and verify calculations
lean_prove
Prove theorems with optional tactics
lean_eval
Evaluate expressions and compute results
lean_type
Check types of expressions
lean_example
Get example code for learning
lean_version
Verify installation status
What You Don't Need
You don't need Mathlib (Lean's advanced math library) for practical finance work.
When to Use Lean
Quick Start Examples
Verify a sum constraint
def weights : List Float := [0.07, 0.30, 0.25, 0.20, 0.15, 0.03, 0.00]
#eval weights.foldl (· + ·) 0.0 -- Should be 1.0Verify a bound
def portfolioPD : Float := 5.98
#eval portfolioPD ≤ 6.0 -- true ✓Verify a formula
def expectedLoss (pd lgd ead : Float) := pd * lgd * ead
#eval expectedLoss 0.05 0.60 1000000 -- $30,000Prove an ordering
theorem gradeA_safer : 1.80 < 16.14 := by native_decide -- ✓The Bottom Line
- Excel errors have cost billions (JPMorgan's London Whale).
- Unit confusion crashed the Mars Climate Orbiter ($327M).
- Rounding errors accumulate silently.
Lean transforms "I think this is right" into
"I can prove this is right."
Get Started with Lean 4 MCP
Requirements
- ✅ Lean 4.26+ installed
- ✅ Works on Windows, macOS, Linux
- ✅ Integrates with existing MCP servers