[isabelle-dev] PlasTeX & blueprint

[Lawrence Paulson]

I’ve just attended a talk about Blueprint, which is used to support the management of large Lean projects. The speaker (Patrick Massot) claims that most of it is system-independent and the specifically Lean part was “a day’s work”. It’s worth looking into.

You start with a LaTeX document containing the material you want to formalise. (Perfect for mathematics manuscripts from ArXiv, at least.) Then you mark it up to indicate dependencies. 

https://github.com/PatrickMassot/leanblueprint
https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/

Larry