This WIP plugin aims to integrate the Lean programming language and theorem prover into Obsidian. The hope is that it will provide a way to work with theories and logic as a natural part of the note-taking experience, much like a Jupyter notebook directly in your notes.
Planned features are as follows:
- Lean running locally in Obsidian via a WASM build.
- Support for the lean infoview to provide interactive assistance while programming.
- The ability to execute lean code blocks in a one-shot or live view, and display results below them. At the same time, the ability to open lean files directly in a standalone editor.
- Support for the language server, including completions, semantic highlighting, hover, and text replacement for symbols.
- Inclusion of the basic libraries, including the bundled standard library, mathlib, and a number of other basic and useful lean libraries.
- Support for lake to assist in working with independent non-notebook projects.
Please note that this plugin is heavily work in progress and may be totally broken at any time. This notice will be removed when things are ready for testing, and updated when there are any actual features implemented.
You can install the plugin using the following two installation methods.
- Go to Settings and select the Community Plugins tab.
- Open the Browse view, and search for "Lean Mode".
- Select this plugin, and press "Install" and then "Enable".
- It should now work!
- Install BRAT.
- In BRAT settings, select "Add Beta Plugin" and paste
https://github.com/iamrecursion/obsidian-leanas the URL. - Go to the "Community Plugins" tab and enable the plugin.
If you are interested in contributing code, documentation, or ideas to this project, please take a look at the CONTRIBUTING guide.