Blueprint for scientific computation

Stream: general

[Terence Tao]

Hi, I am working with Timothy Trudgian and Andrew Yang to create a database of results concerning various analytic number theory exponents (such as growth exponents for the Riemann zeta function). The idea is to record all the known relations between these exponents, and then derive new ones from the old (this mostly involves various linear programming type optimizations). Initially, we are not planning to formalize these derivations in Lean, and instead relying on Python code to support the derivations rather than Lean code, as we are more interested in performing scientific computation than formal verification at this stage. Nevertheless, we are finding the blueprint software to still be useful to organize the project, which can be found here (and here is the blueprint web page). [Thanks to @Pietro Monticone for helping to set up the blueprint software on this repository.]

Of course, blueprint currently has no support for Python, so we are improvising right now with a simple LaTeX macro to supply links to python code after various lemmas in the blueprint (some examples can be found for instance at this chapter of the blueprint). The database is still a work in progress, but the idea is to attach relevant python functions to various computationally intensive lemmas in the blueprint, in analogy to how a formalization project would attach relevant Lean proofs to various blueprint lemmas. This way, any user of the database that wants to try to see what results one would get by combining together various lemmas in the database could start coding in python using the indicated functions.

Anyway, my question here would be whether anyone else has attempted to use the blueprint software for purposes other than a Lean formalization, and whether there are any suggestions on how one could integrate things better. For instance, would it be feasible to add more metadata tags along the lines of the already existing \lean and \leanok to support other languages than Lean?

[Patrick Massot]

Yes, it would be very feasible. I am away from my computer today but I will write more tomorrow. In the mean time, don't hesitate to write more about what you would like.

[Terence Tao]

Well, the improvised solution we have right now is a LaTeX macro that generates a link to a python file, as well as one or more strings of python code that describes what the rough analogue of a given lemma/definition is in python (it may be a class, a function, a function with specific arguments passed, or some other expression).
So one simple option is to upgrade this to an officially recognized metadata tag that the various blueprint visualizations will display when viewing that lemma/definition. (It need not be python-specific: a \code{<file name>}{<line(s) of code>} macro may suffice.)

An alternative is to embed the metadata tags in the python files rather than in the latex files. In this model, one could insert a comment such as # \blueprint{lemma-3.5} at some line of a python file, and then when the lemma tagged \label{lemma-3.5} is viewed in the blueprint, a link will be provided to all the specific lines of code that contain that comment (and maybe a preview of the nearby lines of code could also be provided). This may be a more preferable solution (it requires less manual updating whenever refactoring the code, and also provides ways to navigate back from the python code to the blueprint rather than from the blueprint to the python code). Also I guess one could implement this in any text-based programming language, not just python (the syntax for comments may be different, but blueprint could just search for any lines of code in any language that contained \blueprint{...} somewhere. ). It's possible that that sort of functionality might also be useful in a Lean project as well, although the \lean{} macro already works quite well for such projects.