- Prove mathematical theorems using the Lean interactive theorem proving language side-by-side with your RemNote notes!
- Logic and Proof: An introduction to logic and proof using Lean!
- The Natural Number Game: Build the natural numbers from scratch in Lean!
- Coming Soon: Mathematics for the 21st Century - my intro to logic and proof using Lean and RemNote!
- Tag a statement you would like to prove with the Lean Proof powerup by using the
Lean Proofcommand in the omnibar. - This will open a new pane containing a code editor where you can write your proof.
- The goal state is shown beneath the code editor.
- Whatever you type in the code editor gets saved inside a hidden slot on the Rem.
- Most of the code is adapted from the wonderful Lean Web Editor repository and the Lean VSCode plugin.