Lean 4 Coding Agent
Project Overview
This repository contains an AI-powered agent system that automatically generates and verifies Lean 4 code, turning natural language problem statements into formally proven Lean programs. It's part of a project developed during the LLM Agents Learning MOOC, focused on reasoning, theorem proving, and agent-based AI systems. The system combines multi-agent reasoning with code generation and verification.
Key Features
- Multi-agent collaboration between reasoning and LLM agents
- Automatic generation of Lean 4 code from natural language
- Formal proof verification and theorem proving
- Iterative refinement for error correction
- Integration with GPT-4o and o3-mini models
- Structured analysis and code generation pipeline
Technology Stack
Lean 4
Modern theorem prover for formal verification and mathematical proof
GPT-4o & o3-mini
Large language models for code generation and reasoning
Python
Main programming language for agent orchestration and API integration
Multi-Agent Architecture
Step 1: Reasoning Agent (o3-mini) analyzes problem description and suggests approach.
Step 2: LLM Agent (GPT-4o) generates Lean code and formal proofs.
Step 3: Execution and verification in Lean environment.
Step 4: Iterative refinement when errors are detected.
Course Context
- Developed for UC Berkeley's LLM Agents MOOC
- Led by Professor Dawn Song, Xinyun Chen, and Kaiyu Yang
- Covers inference-time reasoning techniques
- Focuses on autoformalization and theorem proving
Project Gallery