Zulip Chat Archive

Stream: new members

Topic: Iain M


view this post on Zulip Iain Monro (Aug 12 2020 at 10:40):

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 :)

view this post on Zulip Rob Lewis (Aug 12 2020 at 10:48):

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!

view this post on Zulip Iain Monro (Aug 12 2020 at 11:52):

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.

view this post on Zulip Mario Carneiro (Aug 12 2020 at 11:54):

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

view this post on Zulip Patrick Massot (Aug 12 2020 at 11:59):

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).

view this post on Zulip Patrick Massot (Aug 12 2020 at 12:00):

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.

view this post on Zulip Patrick Massot (Aug 12 2020 at 12:02):

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...

view this post on Zulip Mario Carneiro (Aug 12 2020 at 12:06):

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

view this post on Zulip Patrick Massot (Aug 12 2020 at 12:06):

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

view this post on Zulip Patrick Massot (Aug 12 2020 at 12:06):

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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 12:07):

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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 12:07):

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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 12:08):

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

view this post on Zulip Iain Monro (Aug 12 2020 at 12:08):

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

view this post on Zulip Iain Monro (Aug 12 2020 at 12:59):

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?

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 13:09):

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.

view this post on Zulip Mario Carneiro (Aug 12 2020 at 13:11):

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

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 13:12):

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".

view this post on Zulip Mario Carneiro (Aug 12 2020 at 13:13):

easy exercise for the computer, at least

view this post on Zulip Iain Monro (Aug 12 2020 at 14:03):

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.

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 14:04):

Aah I see.

view this post on Zulip Bryan Gin-ge Chen (Aug 12 2020 at 15:11):

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).

view this post on Zulip Patrick Massot (Aug 13 2020 at 21:32):

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.

view this post on Zulip Anatole Dedecker (Aug 13 2020 at 21:57):

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.


Last updated: May 14 2021 at 03:27 UTC