LeanVision

LeanVision is used to extract Lean code from images and PDFs and is built upon the MistralOCR [https://docs.mistral.ai/capabilities/document/].

Installation

To install LeanVision, you can use the following command:

pip install mistralai

Usage

1 - Run in the terminal these commands:

git clone
cd LeanVision

2 - Get your mistral API Key

3 - Run the following command depending on if its the pdf or the image you want to extract the code from. Also note that natively the OCR extracts it into a markdown file, but the script will convert it into a lean file. But if you want it to just be a markdown page, the script will still work and output it as a output.md file. Attached are example images and pdfs to test the script.

python lean4_extractor.py input.pdf output.lean --api-key YOUR_API_KEY 
python lean4_extractor.py input.jpg output.lean --api-key YOUR_API_KEY