When you keep AI Lean, you keep AI correct

Summary of When you keep AI Lean, you keep AI correct

by The Stack Overflow Podcast

25m•August 28, 2026
Listen to Episode

Overview of When you keep AI Lean, you keep AI correct

This episode of the Stack Overflow Podcast explores how the Lean theorem prover and programming language can help make AI systems—especially AI agents—more reliable by requiring them to produce formal proofs of correctness. Guest Leo DeMora (AWS senior principal applied scientist and creator of Lean) explains how Lean is used to verify software, hardware models, and agent policies, and why the combination of probabilistic AI and deterministic formal verification is becoming increasingly practical.

Key themes and discussion points

What Lean is and why it matters

  • Lean is both:
    • a functional programming language
    • a proof assistant for formal mathematics and software verification
  • It allows developers to:
    • write code
    • state what “correct” means
    • prove that the code satisfies that specification
  • A major point: Lean does not automatically know what “correct” means—you must define the desired property first.

Verifying software correctness

  • Leo uses a compression library as a simple example:
    • a key property is that compressing and then decompressing returns the original file
  • In Lean, this property can be stated precisely and proven for all valid inputs.
  • Lean proofs can be lengthy to construct, but they are fast to check once written.

Lean beyond Lean code

  • Lean is not limited to verifying programs written in Lean itself.
  • It can also be used to verify:
    • Rust code via translation tools like Aeneas
    • assembly code through formal models of architectures such as x86 or RISC-V
  • At AWS, Lean is used in contexts such as compiler work and AI infrastructure.

AI agents and formal guardrails

  • The conversation focuses heavily on AI agents and how Lean can constrain them.
  • AWS’s AgentCore and the Cedar policy language were discussed as an example:
    • Cedar policies define what agents are allowed to do
    • Lean is used to verify key properties of Cedar itself
  • This provides a formal way to ensure that if a policy says something is disallowed, it truly is disallowed at runtime.

Why AI and Lean complement each other

  • AI models are probabilistic and good at creative generation, but can hallucinate or make mistakes.
  • Lean is deterministic and can verify outputs.
  • Together, they create a powerful workflow:
    • the AI generates code or proofs
    • Lean verifies them
    • if verification fails, the AI keeps trying

Optimization with proof

  • A major use case discussed is AI-assisted optimization:
    • an agent can be asked to implement a program
    • then optimize it further
    • while continuously proving it still satisfies the original specification
  • This enables developers to explore more aggressive or time-consuming optimizations without manually re-proving correctness each time.
  • Leo shared examples where agents were repeatedly instructed to improve performance while maintaining proofs.

Human role in a proof-driven workflow

  • Developers do not need to become full formal-methods experts to benefit.
  • Leo emphasized that it’s easier to read formal proofs than to write them.
  • Typical workflow:
    • describe the desired behavior in natural language
    • have the AI translate it into Lean
    • review/read the formal specification
    • ask the AI to implement and prove the result
  • Machine assistance can help explain proofs, though users should still be cautious because AI explanations can hallucinate too.

Common failure modes and safeguards

  • The team discussed ways AI-generated proofs can be misleading:
    • proving the wrong statement that merely resembles the intended one
    • adding hidden assumptions that make the proof trivial
    • leaving one important case unproven
  • Lean includes multiple checkers to help catch these issues and prevent deceptive or incorrect proofs from slipping through.

Where proofs help—and where tests still matter

  • Proofs are powerful because they can show a property holds for all inputs, not just tested examples.
  • But testing still has a role:
    • especially for properties outside the logical model, such as memory usage
    • for catching simple bugs before spending time proving something false
  • For low-level systems, memory and stack behavior can be modeled explicitly, but that requires a more detailed formalization.

Notable takeaways

  • “Keep AI lean” means keep it constrained by formal correctness.
  • Proofs can provide peace of mind and allow more aggressive optimization and automation.
  • AI is increasingly capable of generating proofs that used to require specialized human experts.
  • The bottleneck is shifting from checking proofs to discovering them.
  • Leo believes this approach will become mainstream for software, hardware, and security-critical systems.

Closing note

The episode ends with a strong vision for the future: AI agents that can generate, optimize, and adapt code while being continuously checked by formal proofs. Rather than replacing human judgment, Lean gives engineers a way to let AI explore more freely while still enforcing rigorous correctness guarantees.