To simultaneously prove a theorem while formalizing it a link is needed between definitions, lemmas, propositions, theorems etc. in latex with corresponding declarations in lean. To do this I created a tool called span: https://github.com/pachterlab/span 2/

This approach realizes a vision for "machine-readable representations alongside narratives optimized for humans" as advocated for by @sinabooeshaghi and @NeuroLuebbert https://www.biorxiv.org/content/10.64898/2026.01.30.702911v1. Both are important and latex < -- > lean is a perfect example. 3/

I thought about this quite a bit in graduate school, even asking Noga Alon the question once (he gave a partial result on the spot!) It turns out the trivial lower bound can be matched with an elegant application of the probabilistic method. https://arxiv.org/abs/2606.01685 10/

Several people worked on this problem over the years, but it was a minor problem in a small corner of graph theory, so not that surprising that it has been open for a while. Then again, David Moews (first perfect score on a Putnam!) worked on it https://www.sciencedirect.com/science/article/pii/S0012365X9800154X. 9/

So what is span? https://en.wikipedia.org/wiki/Span_(category_theory) It provides a controlled vocabulary for building a “ledger”, which contains “spans” linking the LaTeX, via labels, to Lean, using fully qualified declaration names. 4/

The span tool will check that the ledger is well formed: the LaTeX labels exist, the Lean declaration names resolve, and the resulting paper-facing graph is generated from real Lean dependencies rather than hand-drawn guesswork. 5/

One of my contributions to that paper was defining optimal pebbling and posing the question to determine the optimal pebbling number of a hypercube. 8/ https://pesc.coppe.ufrj.br/~celina/cursos/cps845/PachterCN95.pdf

There's a nice coda that "cooperation is essential", which is fun because this result echoed ideas I've been thinking about in evolutionary biology. https://www.biorxiv.org/content/10.64898/2026.04.07.716994v1 11/11

So what was the paper I used it for? The math is a conjecture about the optimal pebbling number of a cube. It goes back to my first paper which originated from a summer project when I was an undergrad at Caltech working with a postdoc (Hunter Snevily, 1956 -- 2013). 7/

span also facilitates checking that AI generated lean definitions match what is intended in a proof, and also helps to structure and visualize the architecture of a paper. I am finding that it is now an essential tool for all of my projects. 6/

@lpachter This is so cool!

@lpachter @arjunrajlab Fascinating! excited to explore span for verifying math in papers

@lpachter ill be here to read about the tool latex/lean