LeanTeX

A LaTeX package for embedding Lean 4 code directly in LaTeX and rendering Lean's infoview output in the compiled document. The goal is to make formal code feel closer to ordinary mathematical writing. A new release is expected soon.

GraphToTeX

A browser tool for drawing graphs and exporting clean LaTeX/TikZ code. It is built for quick diagramming when a mathematical note needs a graph more than it needs a full graphics workflow.