[sivakon]

This is an interesting usecase, and I want to learn more about your workflow. Do you also use Lean etc. for math proofs.