RemNote Lean

Features

• Prove mathematical theorems using the Lean interactive theorem proving language side-by-side with your RemNote notes!

Resources

• 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!

Usage

• Tag a statement you would like to prove with the Lean Proof powerup by using the Lean Proof command 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.

Example

Credits

• Most of the code is adapted from the wonderful Lean Web Editor repository and the Lean VSCode plugin.