A modern web interface for verifying Lean proofs
Features • Quick Start • Usage • Tech Stack • Contributing
- Monaco Editor - Professional code editor with Lean syntax highlighting
- Real-time Verification - Instant feedback on your Lean proofs via kimina-lean-server
- Smart Error Display - Clear, formatted errors and warnings with precise line/column positions
- Verification History - Automatic saving of all verifications with localStorage persistence
- Node.js 18 or higher
- Docker (for running the Lean verification backend)
-
Clone the repository
git clone https://github.com/yourusername/lean-ui.git cd lean-ui -
Start the backend server
cd backend cp .env.template .env docker compose up -dThis starts the kimina-lean-server on port 10000. Verify it's running:
docker compose logs -f
-
Install frontend dependencies
cd .. npm install -
Start the development server
npm run dev
-
Open your browser
Navigate to http://localhost:3000
That's it! You should see the Lean Runtime Gateway interface ready to use.
# Stop the backend
cd backend && docker compose down
# Stop the frontend (Ctrl+C in the terminal running npm run dev)- Pick a Runtime - Choose a supported Lean 4 + Mathlib runtime (default: Lean 4.9.0)
- Write Lean Code - Enter your Lean code in the Monaco editor
- Add Title (Optional) - Give your verification a descriptive name, or let it auto-generate
- Click Verify - Submit your code for verification
- View Results - See success, errors, warnings, or queued runtime startup status
- Browse History - Access past verifications from the sidebar
- Manage History - Delete individual entries or clear all history
-- Simple theorem
theorem add_comm (a b : Nat) : a + b = b + a := by
rfl
-- Proof by induction
theorem add_zero (n : Nat) : n + 0 = n := by
induction n with
| zero => rfl
| succ n ih => simp [Nat.add_succ, ih]Create a .env.local file in the root directory (optional):
| Variable | Default | Description |
|---|---|---|
KIMINA_SERVER_URL |
http://localhost:10000 |
URL of the kimina-lean-server backend |
KIMINA_SERVER_API_KEY |
unset | Server-side bearer token used by the Next.js proxy; in production this must match Railway LEAN_SERVER_API_KEY |
The backend defaults to Lean 4.9.0. The supported runtimes are Lean 4.9.0, Lean 4.15.0, Lean 4.24.0, Lean 4.27.0, and Lean 4.28.0. Runtime routing is driven by the backend registry. To customize a local runtime service, edit backend/.env:
KIMINA_SERVER_URL=https://lean-ui-production.up.railway.app
KIMINA_SERVER_API_KEY=your-shared-backend-key
LEAN_SERVER_LEAN_VERSION=v4.9.0 # Runtime Lean version
LEAN_SERVER_RUNTIME_ID=v4.9.0 # Runtime registry id
LEAN_SERVER_MAX_REPLS=14 # Max concurrent REPL instances
LEAN_SERVER_MAX_TOTAL_REPLS=14 # Optional process-wide cap across runtime managers
LEAN_SERVER_MAX_WAIT=60 # Max wait time in secondsFor production deployments, set KIMINA_SERVER_URL and KIMINA_SERVER_API_KEY in Vercel project settings. Keep LEAN_SERVER_API_KEY configured on Railway, and use the same secret value for KIMINA_SERVER_API_KEY on Vercel so the frontend proxy can authenticate to /api/check.
See the kimina-lean-server documentation for all options.
- Frontend: Next.js 16, React 18, TypeScript
- Styling: TailwindCSS v4, shadcn/ui
- Editor: Monaco Editor (VS Code editor)
- Backend: kimina-lean-server (FastAPI + Lean REPL)
- Storage: localStorage (client-side persistence)
lean-ui/
├── src/
│ ├── app/
│ │ ├── api/verify/ # API route for Lean verification
│ │ ├── page.tsx # Main application page
│ │ ├── layout.tsx # Root layout with dark theme
│ │ └── globals.css # Global styles
│ ├── components/
│ │ ├── ui/ # shadcn/ui components
│ │ ├── CodeEditor.tsx # Monaco editor wrapper
│ │ ├── HistorySidebar.tsx # Verification history sidebar
│ │ ├── LeanVerifier.tsx # Main verifier component
│ │ └── VerificationPanel.tsx # Results display panel
│ ├── hooks/
│ │ └── useVerificationHistory.ts # History management hook
│ ├── lib/
│ │ ├── nameGenerator.ts # Random name generator
│ │ └── utils.ts # Utility functions
│ └── types/
│ └── verification.ts # TypeScript interfaces
└── backend/ # kimina-lean-server
├── Dockerfile
├── compose.yaml
└── .env # Backend configuration
Contributions are welcome! Please feel free to submit a Pull Request. For major changes, please open an issue first to discuss what you would like to change.
- Fork the repository
- Create your feature branch (
git checkout -b feature/amazing-feature) - Commit your changes (
git commit -m 'Add some amazing feature') - Push to the branch (
git push origin feature/amazing-feature) - Open a Pull Request
- Follow the existing code style
- Use TypeScript for type safety
- Write meaningful commit messages
- Add comments for complex logic
- Ensure Docker is running
- Check if port 10000 is available:
lsof -i :10000 - View logs:
cd backend && docker compose logs -f
- Verify backend is running:
curl http://localhost:10000/api/check - Check
KIMINA_SERVER_URLenvironment variable - Ensure no firewall is blocking port 10000
- Clear browser cache
- Check browser console for errors
- Ensure JavaScript is enabled
This project is licensed under the MIT License - see the LICENSE file for details.
- Lean Prover - The Lean theorem prover
- kimina-lean-server - Fast Lean verification server
- shadcn/ui - Beautiful UI components
- Monaco Editor - VS Code's editor
For questions or feedback, please open an issue on GitHub.