Confluence text

Stream: Equational

[Cody Roux]

We appear to be working at odds in some way: I'm currently writing a chapter on the rewrite theory background, but I see that there is a section on "confluent theories" in Chapter 11: all this is related to issue https://github.com/teorth/equational_theories/issues/555 it would seem. How should we work this out?

[Terence Tao]

Chapter 10.1 was a temporary measure, written to say something about confluence in the absence of a more detailed treatment. If your chapter subsumes the material in Chapter 10.1 then that latter material can be safely deleted (or perhaps portions of it can be retained within your new chapter as appropriate).

[Cody Roux]

Ok cool!

[Cody Roux]

the main issue with my chapter is that there are no references to the lean code (and some cleanup stuff)

[Cody Roux]

I'll make a preliminary PR with the expectation that we can discuss changes here

[Terence Tao]

Alignment with the lean code can always be done later. Actually the blueprint in this project seems to have ended up not to be a critical portion of the workflow in practice - people are formalizing directly from Zulip discussions in many cases; it's more of a reference, and also a potential base for the paper at the end of the project. So the lean integration is a secondary consideration.

[Cody Roux]

That's a relief because the blueprint script mystifies me a bit.

[Terence Tao]

Ideally the project should be as modular as possible: one doesn't need to know all of LaTeX+Blueprint+Lean+Python/Ruby/etc.+Vampire/Z3/etc.+Math in order to contribute, one just needs to know one or two of these things for any specific contribution, and others can fill in the rest later.

[Cody Roux]

Fair, though a poor excuse for me not taking the time to figure it out; I'll work on it tomorrow or Saturday to get it ship shape.

[Shreyas Srinivas]

One flaw with the blueprint approach is that it separates the mathematics from the code. Ideally we should have special latex parsed comments in the lean code that is used to generate the blueprint we see online. It is only slightly different from the way docs works, in that the text in a latex comment need not necessarily be associated with a definition, and the editor must be used to provide proper latex highlighting and completion inside these comments

[Kim Morrison]

Hopefully we can move blueprints to Verso asap! (but not earlier. :-)

[Shreyas Srinivas]

Looking at the examples in the verso repository, it seems there is still a lot of verso specific code to write in addition to the contents of the lean + math file, and it varies from one type of publication format to another.

[Shreyas Srinivas]

Ideally an auto-blueprint tool will read normal lean files, and according to a few config options (for e.g. to only include theorems and not lemmas) generate a doc. There would be a command like lake exe blueprint that does all this. The only extra thing in the normal lean files will be special latex comments containing the math text.

[Eric Taucher]

Kim Morrison said:

Verso

A link would be helpful. :smile:

The first result for a Google search

image.png

which I am sure is not correct. Also did not find anything that seemed correct in the first page of results.

[Mauricio Collares]

It's the first result for "verso lean" here

[Mauricio Collares]

https://github.com/leanprover/verso

[Mauricio Collares]

(see also the talk at https://www.youtube.com/watch?v=dv_vmVs3SQQ)

[Michael Bucko]

Shreyas Srinivas schrieb:

One flaw with the blueprint approach is that it separates the mathematics from the code.

I very much agree with this.
I hope the future of math is agentic and that ML/SW engineers who love mathematics can contribute a lot by building tools, creating and deploying agents, building projects like egg, building models generating tactics, using ml to analyze data etc. , creating and formalizing "claims" (informal theories), developing higher-order languages on top of Lean (or similar) etc.

Keeping math close to code seems like a great idea.

[Terence Tao]

Shreyas Srinivas said:

One flaw with the blueprint approach is that it separates the mathematics from the code. Ideally we should have special latex parsed comments in the lean code that is used to generate the blueprint we see online. It is only slightly different from the way docs works, in that the text in a latex comment need not necessarily be associated with a definition, and the editor must be used to provide proper latex highlighting and completion inside these comments

In the Prime Number Theorem+ project, we used a hack to encode the blueprint as comments inside Lean files; there is a script at compile time that extracts all these comments back out into temporary tex files that become the "classical" blueprint. It works reasonably well, save for the annoyance that VSCode likes to convert various \LaTeX \macros into Unicode.

At the other extreme, in the (still in beta) Analytic Number Theory Exponent Database, we use a blueprint but have 0% Lean code at present; instead, we use some ad hoc macros to link up blueprint theorems with Python code. (The database is set up so that it can in the future be formalized into Lean, but the more immediate purpose is to supply executable (but not formally verified) code to perform various analytic number theory calculations.)

So I think any future version of blueprint should retain a lot of flexibility in how the LaTeX and Lean are to be integrated; there are a lot of different use cases.

[Shreyas Srinivas]

A more robust solution would be to do this with metaprogramming, and adding LSP support to ensure that latex-comments are not processed for unicode inside math-mode delimiters, maybe even rendering them in the infoview. Just like one can synch latex source with the pdf, the infoview would automatically scroll with the cursor position on the source code and show the tactic state where required.

[Shreyas Srinivas]

In principle with some engineering effort it should be possible to render markdown+math and tactic state in the infoview. The trouble with markdown as it exists is getting all the labels and referencing to equation and theorem numbers and lean identifiers.

[Cody Roux]

Historically, this kind of "literate programing" was promoted in the 70s and 80s, but hasn't seemed to gain much traction. Maybe the time is right now though.

[Shreyas Srinivas]

Arguably jupyter notebooks are a form of literate programming

[Shreyas Srinivas]

But we might be able to do better. If we stick to the notebook approach, vscode has a notebook API for extensions. Live rendering lean files + math comments without the jupyter machinery of cells would be even better.

[Cody Roux]

also: I'm happy to have some discussion on the body of the rewriting chapter, it exposes the "classic" theory of rewriting, I intentionally didn't try to conform to what the code is doing exactly, since it felt like a re-discovery of the classic theory with slightly non-standard notations (though kudos to reinventing a whole field of mathematics in a week!)

[Terence Tao]

Probably best to try to align with standard existing notations in the LaTeX side of the project, even if we use some slightly nonstandard terminology on the Lean side.

[Kevin Buzzard]

Instead of using the PNT+ approach I've been writing latex in .tex files in FLT (so I can benefit from VS Code latex plugins) and then copying it wholesale into comments in lean code and hoping that copilot is inspired by it.

[Cody Roux]

That'd be a paper in itself in the right venue (e.g. how often it can come up with something, what mistakes it makes...)

[Shreyas Srinivas]

Writing an extension that upgrades the infoview to a full blown notebook-like view could be a nice ITP paper