Iain M

Stream: new members

[Iain Monro]

Hi all! Introducing myself as per the local custom - I'm Iain, a software developer from the UK. I did an MMath about a decade ago, but decided against doing a PhD in combinatorics for reasons I don't really remember any more, and have been writing code for money ever since.

I have a long running interest in the idea of digitally formalising mathematics, as it's the intersection of two things I understand and enjoy. I've been dabbling in it on the side for a while, going as far as to play with writing my own (rather unpolished) proof assistant / explorer. I'm particularly interested in how to make libraries of formalised proofs explorable, accessible and readable without specialised knowledge, and would very much appreciate pointers to any active work in this area (Lean or otherwise).

At the moment I'm keen just to learn more about Lean and how it works in practice, hopefully by making some contributions to mathlib and getting some experience using it. I look forward to asking a bunch of beginner questions here shortly :)

[Rob Lewis]

I'm particularly interested in how to make libraries of formalised proofs explorable, accessible and readable without specialised knowledge, and would very much appreciate pointers to any active work in this area (Lean or otherwise).

There are definitely people around thinking about this. You may be interested in our recent paper about linting and docs. We're very happy to take feedback about the docs, and even happier to see PRs with improvements!

[Iain Monro]

I actually read that paper yesterday :) I'm definitely on board with the idea of maintaining and expanding docs, and hope to contribute to that to the extent I contribute to the underlying library. But I was trying to get at something more ambitious - the idea that formal proofs in advanced areas could and possibly should be be displayed in a format that is substantially more readable than, say, the current Wikipedia page for that same proof. I'm imagining something like a cross between Metamath's Proof Explorer and the idea of a structured proof, to pick two things I can gesture at that I know actually already exist.

[Mario Carneiro]

If you figure out how to do this, the Metamath crowd will be very interested :)

[Patrick Massot]

Did you look at https://leanprover-community.github.io/format_lean/? (look at the example and click on everything). It's very primitive but already useful (at least for me).

[Patrick Massot]

The basic idea is that you should be able to mix normal text and Lean code, and have access to the tactic state evolving in a proof without installing Lean.

[Patrick Massot]

The idea of structure proof, as implemented in Isabelle, will never be enough to give access to the full information available in a proof assistant. You need something interactive where you can click when you want to see more context, more details, more implicit stuff...

[Mario Carneiro]

The term "structured proof" a la Lamport is different from Isar proofs

[Patrick Massot]

Oh, sorry, I didn't click the link!

[Patrick Massot]

Yes, we want proof assistant helping us to write Lamport's structured proofs.

[Mario Carneiro]

it is more like a proof at many levels of detail, where you can skip the subbranches once you are convinced by the intermediate statement

[Mario Carneiro]

this is definitely what Metamath proofs attempt to do, but unfortunately we haven't learned yet how to do folding well so you have to do that in your own head

[Mario Carneiro]

if you literally read every line of a metamath proof the level of detail is uncomfortably high

[Iain Monro]

Sorry, yes, I added the link to disambiguate the phrase but I should have specified what I meant in actual text!

[Iain Monro]

Patrick Massot said:

Did you look at https://leanprover-community.github.io/format_lean/? (look at the example and click on everything). It's very primitive but already useful (at least for me).

I hadn't seen that, and I was intially excited by it, but it looks like it's just producing the HTML from comments, no? So you just have a non-formal proof interleaved with (and maintained separately to) a formal proof, with no real structural relationship between them. An obvious problem for turning that into a structured proof would be if you wanted to expand out a tricky application of linarith or something . You'd need some way of turning the formal proof that outputs (which is obviously uncommented because it's autogenerated) into readable HTML as well - and once you have that, what do you need the comments for?

[Kevin Buzzard]

The comments are the translation of tactic gobbledegook like linarith which no mathematician understands, into LaTeX, which every mathematician knows and loves. I think they play a key role.

[Mario Carneiro]

yeah, but that's basically saying that the linarith proof is atomic, there is no lower level in the structured proof, even though it's still quite possibly not convincing due to its complexity

[Kevin Buzzard]

linarith is definitely atomic in all the use cases I've ever seen. The translation into LaTeX is "The rest is an easy exercise for the reader".

[Mario Carneiro]

easy exercise for the computer, at least

[Iain Monro]

Kevin Buzzard said:

The comments are the translation of tactic gobbledegook like linarith which no mathematician understands, into LaTeX, which every mathematician knows and loves. I think they play a key role.

I love the idea of translating tactic gobbledegook into readable LaTeX (or at least, readable HTML). I mean, that's the end goal I'm talking about. I just honestly think that the strategy of "do it all manually" would likely turn out to be less feasible than solving the hard problem of doing it automatically.

[Kevin Buzzard]

Aah I see.

[Bryan Gin-ge Chen]

Related to making Lean proofs explorable (though maybe not yet accessible and readable), last year I experimented a bit with writing with embedded interactive Lean code in "Observable notebooks" here: https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums (see also part 2 with some Lean-driven graphics using D3).

[Patrick Massot]

Iain, I understand your concern about tactics that do non-trivial work. But, as far as research-level mathematics is concerned, this is a completely virtual issue. We are very far from having tactics that do steps we would like to see explicit, even in a very detailed proof. Sure, linarith can already do a bit too much when I use Lean to teach first year undergrad, but not much more.

[Anatole Dedecker]

I can confirm, I think linarith will be remembered by every student of this year as the magic tactic. I remember seeing people trying it after every single tactic call, to see if it would help.