Experiments 12
No Goals
Pick a move, see what changes, and keep going until there’s nothing left to prove. Lean checks each step. If you get stuck, try a hint or undo your last move.
Lean 4 · Rust · Axum · Lean REPLView source
Level 01 / Both sides compute
The statement below the line is your goal. Here, you need to prove that 2 + 2 = 4. Try a move to see how Lean checks it.
You have
Loading the goal from Lean…
You need
- ⊢
- what you need
Notes
The board shows the goals and error messages returned by Lean 4.34. The explanations above it help you read the results as you go.
How a check works
A Rust service runs Lean through the Lean REPL. When you try a move, it checks your proof from the beginning, including the new step. Your progress is saved in this browser, so you can come back to it later.
What you can type
The box accepts any single tactic from core Lean, without Mathlib. It rejects sorry, compiled evaluation such as native_decide, and anything that reaches outside the proof. Each move has five seconds before the process is replaced. The levels use rfl, decide, exact, intro, obtain, constructor, left, right, rw, induction, and omega.