A newcomer's opinion

Stream: general

[Adrian Chu]

I am still very new to lean but I have been browsing through mathlib these days. I would like to share one obstacle I observed that an ordinary mathematician would face when trying to understanding lean code. That is, abbreviation of mathematical terms. For example, look at this definition of an outer measure:

structure outer_measure (α : Type*) :=
(measure_of : set α → ennreal)
(empty : measure_of ∅ = 0)
(mono : ∀{s₁ s₂}, s₁ ⊆ s₂ → measure_of s₁ ≤ measure_of s₂)
(Union_nat : ∀(s:ℕ → set α), measure_of (⋃i, s i) ≤ (∑i, measure_of (s i)))

In this case, since I am familiar with the definition, I can guess that ennreal = extented non-negative reals, mono=monotonicity, Union_nat= countable subadditivity. But others might get it. Moreover, sometimes the abbreviation is long and odd looking and it's hard to guess its meaning. I understand that abbreviation can shorten the code, but I would argue that in the statement of major definitions or theorems, it worthes avoiding abbreviation in order to increase the readability to ordinary mathematicians.

[Chris Hughes]

If you hover over ennreal it should tell you what it is.

[Adrian Chu]

If you hover over ennreal it should tell you what it is.

I can't see it in mathlib. But even if so, there are still many examples of abbreviation causing confusion.

[Mario Carneiro]

The naming follows a somewhat rigid convention in order to make it easier to guess the names of theorems. Mathematicians are not globally consistent in how things get named, so if you try to follow that kind of pattern you end up confusing even yourself after a while

[Mario Carneiro]

For the particular case of fields of outer_measure, I wouldn't associate much to the particular names. It's just a bunch of axioms

[Mario Carneiro]

For example in most presentations of, say, vector spaces you find in textbooks it's just a list of equalities. You can give them names, but they aren't that helpful

[Mario Carneiro]

It's true that it is somewhat of an idiolect that you have to learn, but there is no way around that. Using mathematician naming for the things that mathematicians bothered to name would just make it a more inconsistent language

[Adrian Chu]

could you explain the rigid convension a bit?

[Mario Carneiro]

https://github.com/leanprover-community/mathlib/blob/master/docs/naming.md

[Kevin Buzzard]

With a version of the perfectoid project up until a few weeks ago, we had specifically tried to make our definition of a perfectoid space readable by mathematicians. More recently we've been trying to actually get it to compile, and now it is probably less readable (and still doesn't compile), however it is still pretty readable, indeed it's more readable than it was yesterday morning, and one high priority issue after we get it working will be to make it better readable.

[Kevin Buzzard]

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/perfectoid_space.lean

[Kevin Buzzard]

/-- A perfectoid ring, following Fontaine Sem Bourb-/
class perfectoid_ring (R : Type u) [Huber_ring R] extends Tate_ring R : Prop :=
(complete : is_complete_hausdorff R)
(uniform  : is_uniform R)
(ramified : ∃ ϖ : pseudo_uniformizer R, (ϖ^p : Rᵒ) ∣ p)
(Frob     : ∀ a : Rᵒ, ∃ b : Rᵒ, (p : Rᵒ) ∣ (b^p - a : Rᵒ))

class perfectoid_space (X : Type u) [topological_space X] extends adic_space X :=
(perfectoid_cover : ∀ x : X, ∃ (U : opens X) (A : Huber_pair) [perfectoid_ring A],
  -- next hypothesis is always true although we're yet to prove this
  (x ∈ U) ∧ nonempty (𝒞.equiv (𝒞.Spa A : 𝒞 (Spa A))
    ((locally_ringed_valued_space).to_𝒞.restrict U : 𝒞 U)))
-- is_preadic_space_equiv U (Spa A))

Perfectoid ring is not bad really. Note that one difference is that perfectoid_ring is written by mathematicians, and outer_measure was written by computer scientists.

[Kevin Buzzard]

Johan says outer measure isn't really that bad either -- there is obviously an initial learning curve when it comes to the basic definitions. One can also define notation to fix these problems. How would you like to express ennreal? Any unicode stuff we can do.

[Adrian Chu]

@Kevin Buzzard For ennreal, how about [0,∞] ? Also, in some cases when we don't have such compact notation, why not use the full name, e.g. extended_non_negative_reals?

[Kevin Buzzard]

Computer scientists don't like long names because they are boring to write.

[Adrian Chu]

yes, but readability is sacrificed in my opinion

[Adrian Chu]

e.g. when we look at the command of mathematica, they rarely use abbreviation

[Greg Conneen]

I'm gonna agree with Kevin here and say that while long, pretty names are quite nice when you're new and trying to understand the material, there's always going to be a learning curve for reading code when it comes to any language. As long as there's some note at the construction saying that ennreal is the extended non-negative reals, abbreviation is more than acceptable. It gets quite tedious trying to use a certain object over and over again when referencing it takes more than 10-15 characters to type.

Mathematica isn't really a good analogue, because it's not a language in which you're typing dozens of lines of code. A lot of mathematica is note-taking and use of wolfram alpha.

[Greg Conneen]

Furthermore, mathematica's code is almost purely computational. You don't have to write out the same words hundreds of times. If refl were reflexive_property and simp were simplify_goal, we'd all go crazy

[Adrian Chu]

ya, i agree that there should be a package of abbreviation that we need to remember. abbreviation in proofs are certainly needed. i just think that we could pay attention to have a balance between brevity and readability, especially in major definition and theoems

[Adrian Chu]

because part of the goal of lean (in the future) is that, mathematician who does not specialize in lean, can still use lean

[Adrian Chu]

by "use", i mean they can look at the relevant definition and theorems when needed

[Greg Conneen]

That sounds like an unnecessary mess to deal with. If we're going to define a theorem name, we should do it for usability. Why would you make a naming convention that you're never going to use, and instead overwrite it?

[Patrick Massot]

I guess if you think abbreviations are a major problem then you haven't try to do anything yet...

[Patrick Massot]

There are actual difficulties in using a proof assistant, and getting used to ennreal is not one of them

[Greg Conneen]

I agree that it's important for mathematicians to be able to use Lean, especially since I'm one of them. But just like you said in the very beginning, you could already guess what the ennreals are because you were familiar with the construction. Which shows the convention works. And if you aren't familiar with the construction in mathematics, you probably aren't ready to be messing around with it in Lean.

[Adrian Chu]

OK, I'm convinced :)

[Adrian Chu]

this's an outsider's view, as the title stated

[Adrian Chu]

when i become an insider of lean, this view will certainly be changed

[Johan Commelin]

@Adrian Chu What we could is write a lot more docstrings. Those are comments in the code that show up when you hover over a term in VScode. (So hovering your mouse cursor over ennreal would show a box saying: "The type of non-negative reals with positive infinity". Maybe it even already does that.) Reading Lean code outside of a proper IDE is pretty unusable anyways, but inside VScode (or Emacs) this could be fairly usable. However, lots of things don't currently have docstrings.

[Chris Hughes]

I would like a glossary or something like that. The idea is to look up a maths thing, and find out what it's called in Lean, and maybe the most basic peculiarities you need to be aware of to use it. So if someone wants to think about linear combinations, then they know they're called finsupp.

[Jan-David Salchow]

This kind of thing could be generated from docstrings

[Jan-David Salchow]

In general it would be amazing to have some documentation extracted from lean code automatically

[Jan-David Salchow]

Is somebody working on this kind of thing?

[Johan Commelin]

@Fabian Glöckle mentioned a wonderful idea to me over dinner. We now have AI's that generate captions for images using image recognition. Fabian suggested we train an AI to generate high-level explanations of proofs from Lean source code.

[Simon Hudon]

@Jan-David Salchow Are you talking about something of the kind of JavaDocs or Doxygen?

[Simon Hudon]

I've been working on a linting tool for a couple of weeks. Right now, it tries to sanitize imports but if we can find a criterion for which theorems should have documentation, I could have the tool enforce the rule

[Johan Commelin]

I've no clue what such a criterion should look like.

[Mario Carneiro]

I once went through mathlib and added docstrings to every def, inductive, and class. It would be nice to have comments on all theorems but that's an order of magnitude more work

[Simon Hudon]

We can enforce every def inductive and class for starter

[Greg Conneen]

I think the easiest way to make a document accessible is to make a text defining everything the file does, but on paper, then proving the theorems on paper in an analogous way to the lean document. That way, every document has a readable file in plain mathematical english, which can be directly translated to and from the Lean code

[Greg Conneen]

However, doing something like that for even one document in mathlib would take some serious doing.

[Greg Conneen]

I suppose I'd be interested in undertaking something like that, as I would be learning a lot about Lean in the process

[matt rice]

I looked a little at a doxygen/javadocs esque thing, one thing to note is that e.g. docstrings are in the olean files, so available from Mario's olean-rs, When looking at it I was wondering if it wouldn't be possible to do Patrick's format-lean in docstrings, which I view much as like what Greg mentions above, but in source code comments rather than an external file.

The issue there was that docstrings weren't available in the proof contents you cannot have a docstring for a have statement. E.g. docstrings get associated with a symbol, I didn't see a way to associate them with a file:line location as well. Anyhow i felt the whole thing would probably be outdated once the lean4 parser in lean came along anyways, should revisit it I suppose.

[Adrian Chu]

I would like a glossary or something like that. The idea is to look up a maths thing, and find out what it's called in Lean, and maybe the most basic peculiarities you need to be aware of to use it. So if someone wants to think about linear combinations, then they know they're called finsupp.

@Chris Hughes I think this is a very good idea.

[Adrian Chu]

I think the easiest way to make a document accessible is to make a text defining everything the file does, but on paper, then proving the theorems on paper in an analogous way to the lean document. That way, every document has a readable file in plain mathematical english, which can be directly translated to and from the Lean code

@Greg Conneen I think we don't need this for everything piece of code, since most definitions and statement of theorem have very readable lean code, at least when a "dictionary" for the abbreviations of relevant terms is provided. We probably only need a readable plain english text to summarize the length and complicated proofs.

[Adrian Chu]

I noticed another issue. Every lemma in lean code has a name, like mem_gpowers_iff_mem_range_order_of, sum_card_order_of_eq_card_pow_eq_one. These names only make sense only after looking at the statement of the lemma. An innocent thought: why don't we just use numberings like lemma_12, together with a longer and more readable comment? In this way, when we later need to quote this, we can type much less; and we no longer need to guess what the string of abbreviation means.

[Mario Carneiro]

nooooo

[Adrian Chu]

For major definition and theorem, of course, we should give it a proper name. But for small lemma, why not just use numbering?

[Mario Carneiro]

because you see that lemma in places completely elsewhere

[Adrian Chu]

But

[Mario Carneiro]

These names only make sense only after looking at the statement of the lemma

Those names literally say what the statement is

[Mario Carneiro]

admittedly, for the more complicated statements it's difficult to render as text, but it at least gives a strong hint what the statement is

[Adrian Chu]

But the strategy I mention is used in every mathematical paper...

[Mario Carneiro]

yes, I know that mathematicians can't name things

[Adrian Chu]

well they don't name small lemmas

[Mario Carneiro]

almost every theorem in mathlib is a small lemma by mathematician standards

[Mario Carneiro]

I cannot stress how completely unreadable this would render the library

[Adrian Chu]

because you see that lemma in places completely elsewhere

To solve this, whenever this lemma is quoted elsewhere, we can have a link to the original one?

[Mario Carneiro]

we already have that

[Mario Carneiro]

the amount of cross referencing you would need to do to read anything would go up by an order of magnitude

[Mario Carneiro]

we no longer need to guess what the string of abbreviation means

Instead of guessing what the string of abbreviation means, you now have to guess what a number means. Humans aren't compilers

[Adrian Chu]

I see. I understand.

[Adrian Chu]

Maybe a better proposal is like this: we use abbreviations as names of lemma, but we also write a comment, which expands the abbreviation, for every lemma. And wherever this lemma is quoted, we can see that comment for an explanation by hovering on its name.

[Kevin Buzzard]

What you don't see is that what to you looks like a useless lemma name is to me an absolutely crucial method for funding the lemma. Once you can start to begin to guess what technical lemmas are called, you can find them by guessing half the name and then using basic search functionality like ctrl-space. I actually use the fact that these lemmas are named well as part of my workflow and, in contrast to my initial instincts, I now believe that the system scales well. In my formalisation of parts of the stacks project I deviated from the computer scientist's advice in naming things (files in this case -- I used stacks projects tags) and it was a disaster. This is analogous to rejecting the suggestion that chapters of a book should be called chapter 1, chapter 2 etc. We all do it but it turns out to be a terrible idea now better naming conventions are available

[Adrian Chu]

I see..

[Johan Commelin]

@Adrian Chu Instead of hovering, you can Ctrl-click to open a new tab, or you can click (so that your cursor is blinking on that symbol) and then hit Ctrl-Shift-F10, to get a pop-up showing the 15 lines of context around the def/statement of that symbol.

[Mario Carneiro]

we also write a comment, which expands the abbreviation, for every lemma. And wherever this lemma is quoted, we can see that comment for an explanation by hovering on its name.

If the only purpose of the comment is to expand the abbreviations in it, then that's not a very good comment. It's like the infamous

i = i + 1; // add 1 to i

which says what the code says without adding anything. Comments are to provide information that can't be gleaned from the code itself, like relations to other concepts, alternate names, references to the literature, and architectural comments

[Mario Carneiro]

When you hover over a lemma name, lean will show the statement of the lemma, which mostly addresses the question of "what does this theorem assert?". If the statement is long or complicated, then an english gloss is helpful for connecting it to standard mathematical terminology. Actually I think english glosses are usually a good idea, since the duplication of the statement in two different languages can help reinforce the concept. But if it can be generated automatically then it's a rubbish comment

[Adrian Chu]

Yeah, surely we don't always need a comment

[Mario Carneiro]

The last theorem prover I worked on, Metamath, has a style rule that all theorems must have a comment. It doesn't have to be much, but there has to be something. This is remarkably effective at generating pervasive documentation

[Mario Carneiro]

The ship has probably sailed on doing that for mathlib though

[Adrian Chu]

Maybe I was not focusing on the practical point of view. I was thinking how to make lean code presentable and easy to advertise to outsider mathematician :)

[Mario Carneiro]

I think lean code is more readable than many theorem provers, but formalization necessitates some level of pedantry that can interfere with mathematical readability

[Adrian Chu]

Human language is highly readable and efficient but full of inconsistence and inaccuracy; code is vice versa. It is tricky to find the balance.

[Mario Carneiro]

Also I think that computer languages that rely too heavily on natural language processing tend to be difficult to use

[Mario Carneiro]

For writing code, you really want the language to have a limited lexicon, to keep it easy to learn

[Mario Carneiro]

So I reject the premise that the optimal programming language is a natural language

[Adrian Chu]

Agree. The main purpose of a math paper is to communicate. On the other hand, I am not sure to what degree is the communication of mathematical ideas a purpose of Lean code.

[Johan Commelin]

Right... It may be very hard to create a mathematical document that is useful as:

• certificate of correctness of the theory
• reference text for those who know the theory
• teaching material for those who don't know the theory

But we can still strive to get at much of that as possible. Only Lean will not let us compromise on the first item.

[Kevin Buzzard]

The ship has probably sailed on doing that for mathlib though

I don't believe that at all.

[Adrian Chu]

btw, does anyone has a vision of how we will categorize the files in mathlib when it grows larger in the future? Will we adopt the AMS Mathematics Subject Classification?

[Patrick Massot]

This was discussed, but this AMS classification is really bad. Clearly it wasn't designed with this goal in mind

[Scott Morrison]

The ship has probably sailed on doing that for mathlib though

I don't believe that at all.

I agree --- let's institute a rule like this. Could we ask that _every_ declaration in new PRs should have a docstring?

[Simon Hudon]

That sounds overkill. Many lemmas have a sufficiently explicative name

[Simon Hudon]

We could say: types, classes and (public) definitions at least.

[Alexander Kurz]

As a newcomer myself, I would agree with Adrian Chu's initial opinion. Two more thoughts. First, whenever one has to weigh readers against writers, shouldn't one side with the readers? In the end, isn't the hope that every theorem will be read much more often than written? That more time will be spent, overall, reading a theorem than writing it? Second, when it comes to the pain of writing long names, don't modern editors take the burden away from the writer by offering a list of possible completions?

[Simon Hudon]

I don't agree. Some theorems are worth reading but many are really just one item a long list of rewrite rules

[Andrew Ashworth]

also, java style long names are also terrible to read in their own way, once you start having the majority of your lines fail to fit in 80 or 120 chars

[Simon Hudon]

Are you talking about Lean 4?

[Andrew Ashworth]

no, i'm referring to the reader vs writer (long name) discussion

[Simon Hudon]

Ok but the difference between names and doc string is that no matter how long your doc strings are, it won't affect the readability of the definitions that uses it

[Andrew Ashworth]

sure. is that what '... Adrian Chu's initial opinion.' was referring to?

[Andrew Ashworth]

I am all for long docstrings!

[Kevin Buzzard]

Adrian Chu's initial post referred to this piece of Lean code:

structure outer_measure (α : Type*) :=
(measure_of : set α → ennreal)
(empty : measure_of ∅ = 0)
(mono : ∀{s₁ s₂}, s₁ ⊆ s₂ → measure_of s₁ ≤ measure_of s₂)
(Union_nat : ∀(s:ℕ → set α), measure_of (⋃i, s i) ≤ (∑i, measure_of (s i)))

This is the Lean definition of outer_measure. As you can see from the link, there is absolutely no context or even a docstring. Several suggestions have been made about how to make this definition more readily accessible to passing mathematicians. Not all of them are viable -- for example changing constructor names breaks code, and to a computer scientist (and this code was written by a computer scientist) there is nothing wrong with the names anyway -- in fact several of them are the canonical names for what they are doing. Mathematicians don't know this part of the story though. Adrian can only understand the definition because he has seen the definition in more mathematician-friendly places, e.g. a book, or Wikipedia or something -- something which was written to be read by humans. This code was not. However as a human myself, I did once try to learn what mathlib was all about by reading mathlib and I found it extremely difficult to get anywhere. In the end I learnt what it was about by taking mathematics I understood, like the definition of a scheme, and trying to write it in Lean. But we can do better in this instance.

How would the maintainers feel about a small PR containing only comments about what was going on in this definition, and perhaps a reference to the literature or Wikipedia?

[Adrian Chu]

1. Do the creator/contributors of mathlib have a common consensus on, in the long run, (a) who is the target reader/user of mathlib?, (b) what are all the purpose of mathlib? In my opinion, having a clear answer to these 2 questions would tell us what style should lean code adopt.
2. The following is about promotions of lean. Please keep in mind that, something with little practical value (say, from a programmer's point of view) could have significant promotional value. People's reluctance to use or learn something (lean in this case) is often emotional. Consider the fact that in this early stage, people really don't have much incentive to learn/use lean, I would argue that any writing style of lean code that brings clarity and transparency would be a big attractive factor to outsiders.
3. Following point 2. Newcomers of lean certainly do not install lean immediately, they will probably first poke around and look at mathlib through github. But in github, we can't see any of the docstring or link to definition, etc. So from a promotional point of view, this is no good.

[Kevin Buzzard]

I think the target user and reader of mathlib is a computer ;-) The purpose of mathlib is that it is a tool to help humans formalise definitions of objects and statements and proofs of theorems, with the ultimate goal of changing the way mathematicians work -- for example, supplying them with better search tools. But the humans formalising the definitions need to be trained, and they need to be trained to read mathlib, at least if mathlib stays as it is.

[Kevin Buzzard]

I posted our definition of a perfectoid space and to a programmer this has little practical value but I personally believe that there will be a lot of promotional value at least in mathematics departments. This is not really the computer scientists' job though. They need to ensure that they have a library which compiles without too much trouble and provides a solid API for most of the things it claims to be offering.

[Kevin Buzzard]

I think that the mathlib devs already have a clear idea of what they think mathlib should look like, and that's why it looks like what it looks like. They have already made it quite clear to me that they do not want long clear proofs of simple statements; they would rather have obfuscated one-liners (not least because they probably compile quicker).

[Kevin Buzzard]

Currently, it is a bad idea directing mathematicians towards mathlib; it is incomprehensible and poorly-documented. We need to direct them elsewhere.

[Adrian Chu]

Currently, it is a bad idea directing mathematicians towards mathlib; it is incomprehensible and poorly-documented. We need to direct them elsewhere.

Agree, mathematician's participation in mathlib is probably something in the distant future

[Kevin Buzzard]

The Xena project has a bunch of material which might be much easier to read, however it is all undergraduate level. This might not matter though -- my experience is that most staff are far too busy to be thinking about learning a new language. The undergraduates are more likely to be reading mathlib than the staff, in a maths department. This is why we need more teaching material which is accessible to undergraduate mathematicians.

[Johan Commelin]

Otoh, we've thrown some bright young students at mathlib, and they seem to do just fine. So maybe the older generation is just too old and lazy to learn something (-;

[Kevin Buzzard]

Agree, mathematician's participation in mathlib is probably something in the distant future

You say that -- but look at Hales, look at me, look at Patrick, look at Johan.

[Kevin Buzzard]

And look at people like Neil Strickland, who contribute sometimes. Take-up is slow, but non-zero. However amongst the students I see far more enthusiasm. They don't read mathlib though, they tend to look at materials that I make, or learn from each other. They certainly use mathlib though.

[Johan Commelin]

Some students also read mathlib: Chris Hughes, Kenny Lau, Fabian Glöckle, and more...

[Jesse Michael Han]

learning to read/use mathlib is definitely a skill by itself---we're planning some lectures at this year's formal abstracts summer school specifically about 1) familiarizing yourself with existing libraries and 2) building your own library (this includes things like best practices for simp lemmas, etc)

[Johan Commelin]

Ooh, and we should also mention Reid Barton and Scott Morisson, if we are listing "mathematicians turned to Lean"...

[Patrick Massot]

Agree, mathematician's participation in mathlib is probably something in the distant future

@Adrian Chu there may be some misunderstanding here: Kevin, Johan, Sébastien and I have absolutely no training in computer science or software engineering. If we are not mathematicians then I don't know who is, unless you require a Fields medal or some other really big prize to qualify as a mathematician.

[Johan Commelin]

Wait, Patrick... you don't have a Fields medal?

[Patrick Massot]

and, as Johan pointed out when I was writing, my list is not exhaustive

[Patrick Massot]

Technically it's not too late

[Patrick Massot]

or maybe it is. When is the next congress?

[Johan Commelin]

2022?

[Patrick Massot]

Crap. I'll be 41

[Patrick Massot]

Let me do formalized math instead

[Adrian Chu]

Agree, mathematician's participation in mathlib is probably something in the distant future

Adrian Chu there may be some misunderstanding here: Kevin, Johan, Sébastien and I have absolutely no training in computer science or software engineering. If we are not mathematicians then I don't know who is, unless you require a Fields medal or some other really big prize to qualify as a mathematician.

Sorry for the miscommunication. I meant to say "LARGESCALE participation by mathematician". Let's imagine someday lean is so popular that lots of mathematician uses it. The best case scenario I can imagine is that mathematician use lean to formalize the STATEMENT of the theorems they discovered and then add it into the mathlib database. When the foundational material of mathlib is sufficient, I can imagine that it wouldn't take much effort to do so.

[Jesse Michael Han]

The best case scenario I can imagine is that mathematician use lean to formalize the STATEMENT of the theorems they discovered and then add it into the mathlib database.

maybe you should have a word with tom hales: https://formalabstracts.github.io/

[Adrian Chu]

The reason I think it won't take too much effort is that, when I show to my friend (a math graduate student who haven't seen lean before) the lean code of definitions of, say, the Hausdorff topology or outer measure, he easily understand the rough meaning of the code.

[Moses Schönfinkel]

Perhaps one should also keep in mind that Coq has been around for three decades and has yet to see widespread adoption. Lean is technically more readable but not to the extent to turn itps into the new thing, at least not without "too much effort".

[Moses Schönfinkel]

So whilst I definitely don't want to diminish your optimism and enthusiasm, evidence and historical data so far suggests a different scenario :).

[Adrian Chu]

I said a mathematician writing the code of definition/statement won't take much effort, I didn't said popularizing lean won't take too much effort :)

[Adrian Chu]

Making lean useful to ordinary mathematician will surely take lots of effort

[Kevin Buzzard]

So whilst I definitely don't want to diminish your optimism and enthusiasm, evidence and historical data so far suggests a different scenario :).

I think that Coq has been very poorly marketed [to the maths community] by the CS community. I think that this is because the CS community has no idea what makes the maths community tick. The proof of the odd order theorem shows us that formal proof verifiers are capable of understanding several hundred pages of lemmas about group theory. This is a really useful data point for the CS people. But mathematicians don't care about the maths -- this is 50 years old and well-known, it is a major result in what is now regarded as a dead area. This is my question to the Coq community -- where are all the modern research level objects which get mathematicians excited? Where are the formalisations of the Millennium problems? Where are schemes? Where is all the stuff that research mathematicians are interested in? I looked and looked and I can find very little. In Lean we are doing things differently. The development of the maths library is now in general being done by people who have mathematical goals -- for example I want to formalise the global Langlands conjectures so am gently pushing people to do algebraic closure of fields, Galois theory, group cohomology, global fields etc. These things might just all be done in random places in Coq Contribs or whatever -- or maybe they're not even there at all. In fact I am certain that the Langlands conjectures are not there -- because this isn't the kind of thing that was getting done in Coq. I am not even sure there is a human alive on this planet who knows enough about Coq and enough about the Langlands conjectures to be able to even write the code. We are driving the Lean maths library project towards objects which real mathematicians actually care about. Once we have a large collection of these things, we will look completely different to Coq because our library will reflect a much more modern mathematics. So I reject the argument that says that history is not on our side.

[Kevin Buzzard]

I said a mathematician writing the code of definition/statement won't take much effort, I didn't said popularizing lean won't take too much effort :)

This is the first step. But first we need to build the definitions. When I can go round to the people in my department and say "tell me a theorem / conjecture you're working on or thinking about" and I have about a 50% chance of being able to formalise this theorem painlessly in Lean, that's when people are going to start listening. I have a clear path towards this -- get undergraduates formalising things like calculus and manifolds and basic stuff, and then get PhD students formalising harder stuff. This is where to start. The staff don't care and are stuck in their ways. The revolution is going to come from a very surprising source -- kids. Once we can actually state things like the Hodge Conjecture -- and it will only be a couple of years, believe you me -- and once we have a database of human-claimed theorems and can begin to make a database which can be used for search -- then they will come. They're not here now because we have nothing to offer them yet. But I can see this changing very quickly if I can keep the momentum going.

[Kevin Buzzard]

I am still pretty convinced that I have epsilon chance of being able to formalise anything any of my colleagues tell me they're working on at this point.

[Kevin Buzzard]

Making lean useful to ordinary mathematician will surely take lots of effort

People will get money and it will happen. Look at Hales. Doing anything takes lots of effort -- and yet things happen. It's like saying "Writing Microsoft Windows will take lots of effort". Sure. And yet it got written.

[Alexander Kurz]

Currently, it is a bad idea directing mathematicians towards mathlib; it is incomprehensible and poorly-documented. We need to direct them elsewhere.

Thanks for this clear statement. This sounds to me as if another layer of interface on top of mathlib was needed. Has anybody been thinking about how to do something like this? An interface that would allow a mathematician to use lean without having to access mathlib?

[Kevin Buzzard]

I think this is a really interesting question. Patrick has been working on some wonderful ways of presenting Lean code so that mathematicians can see relevant parts of it -- for example I wrote this proof of the sandwich theorem to show my undergraduates, and if you click on a line in the proof and then click on one of the small grey boxes which appear, you will be able to see Lean's tactic state at that point in the proof. Mathematicians can understand the tactic state, and if we work harder with notation (which Lean 4 will enable us to do) we will be able to make it even easier for them to understand.

[Kevin Buzzard]

Let me stress that whilst that is my Lean code, it's Patrick's formatter which makes it look so good.

[Kevin Buzzard]

And Lean 4 will enable us to make it look even better. However I do not know how to make this interface that you're talking about to enable mathematicians to write Lean code. Let's face it -- even if we had some mega version of Patrick's formatter which made mathlib just look like a maths book -- that won't help mathematicians to be able to write Lean code, which will still look like intros x, apply eq_of_ne_of_supremum_positive, ...

[Kevin Buzzard]

The only solution I can see so far with getting mathematicians to use Lean is to actually teach them how to write proofs in tactic mode. Once we have more mathematical objects and conjectures we can start thinking about how to interact with the software in other ways -- for example, via search. Then this will give mathematicians new ways of being able to benefit from the software without having to learn how to write Lean code. That's what we want, really. Until then we need to train people to be able to write Lean code.

[Mario Carneiro]

I think we should work more on getting leandoc working. It's been planned forever, but having an HTML view of mathlib would make things much nicer for the casual user

[Kevin Buzzard]

Can you explain what leandoc is?

[Mario Carneiro]

It's like javadoc or haddock or any other documentation system for code... Take all the specially marked /-- comments and turn them into HTML files

[Simon Hudon]

And add hyperlinks between definitions and types.

[Kevin Buzzard]

I don't know what javadoc or haddock are either, but I can now begin to guess.

[Kevin Buzzard]

So it just means people can look at Lean code without having to use VS Code and they can still get the "right click functionality"?

[Simon Hudon]

Yes and I think we can have text when hovering over types and definitions

[Kevin Buzzard]

Would there be a way of incorporating LaTeX into things somehow, via MathJax?

[Kevin Buzzard]

Mathematicians are a bit turned off by things if they're not in LaTeX.

[Adrian Chu]

I said a mathematician writing the code of definition/statement won't take much effort, I didn't said popularizing lean won't take too much effort :)

This is the first step. But first we need to build the definitions. When I can go round to the people in my department and say "tell me a theorem / conjecture you're working on or thinking about" and I have about a 50% chance of being able to formalise this theorem painlessly in Lean, that's when people are going to start listening. I have a clear path towards this -- get undergraduates formalising things like calculus and manifolds and basic stuff, and then get PhD students formalising harder stuff. This is where to start. The staff don't care and are stuck in their ways. The revolution is going to come from a very surprising source -- kids. Once we can actually state things like the Hodge Conjecture -- and it will only be a couple of years, believe you me -- and once we have a database of human-claimed theorems and can begin to make a database which can be used for search -- then they will come. They're not here now because we have nothing to offer them yet. But I can see this changing very quickly if I can keep the momentum going.

About mathlib database being used for searching in the future: how would it be better/more convenient/more efficient than wiki+google+arxiv?

[Johan Commelin]

@Adrian Chu Try library_search

[Johan Commelin]

You write down your result, and Lean figures out the name (iff it is in the library)

[Johan Commelin]

The infrastructure is there, now we just need to fill the database with maths.

[Johan Commelin]

People are working on tools that try to generate counterexamples to your statement

[Johan Commelin]

Besides checking if a result is literally in the library, we can have lightweight automation check if it is a trivial variant/combo of results in the library

[Adrian Chu]

Besides checking if a result is literally in the library, we can have lightweight automation check if it is a trivial variant/combo of results in the library

People are working on tools that try to generate counterexamples to your statement

Wow, I know these 2 are some of the main purposes of having a database, but I thought they will only be achieved in the very distant future...

[Kevin Buzzard]

Does using Wikipedia + Google + ArXiv really work? I've had MSc students coming into my office brandishing printouts of 5 page pdfs which they found using Google when trying to answer a technical question, and the pdfs were written by PhD students perhaps as notes for a talk they had to give on material they didn't understand, and the notes are full of crap but this is not easy for my MSc student to figure out because it's in LaTeX so looks nice

[Kevin Buzzard]

Can you find a proof in the literature that every complete intersection ring is Cohen--Macauley using Google and Wikipedia and ArXiv? And even if you can, could you imagine a world where this question would not even be worth considering because the answer was "obviously yes"? If I were to ask you if it was possible to find a picture of a china teapot on the internet you would say "of course!'. It is completely trivial to do now. But I remember a time when it was impossible to do.

[Adrian Chu]

Ah, I see what you mean. Mathlib can serve as a database of small, specific, technical lemma. I think the reason why we can't find proof of technical lemmas in literature is that no one bothers to write them down: the experts think they are well-known and can be easily derived.

[Adrian Chu]

So in your mind, how will the statement or proof of these specific, technical lemma come into existence in mathlib in the future?

[Johan Commelin]

Through a combo of hard work and automation

[Kevin Buzzard]

Not just technical lemmas necessarily -- theorems announced in the literature whose proofs are not formalised. Once we have enough definitions with sufficiently good API then mathematicians will be able to start making their own definitions. At the minute it is really hard to make a meaty definition in Lean -- witness the fact that it just took a team of us months and months to do perfectoid spaces. But once we have a robust theory of "most normal things" it will get to the point where a mathematician can say "do you have separable Banach spaces? I want to state a result about them" and we say "well, we have Banach spaces, but nobody mentioned separable ones before, hang on, let me write one line of code, Ok now we have separable Banach spaces"

[Mario Carneiro]

I don't see a reason to believe that this will ever be one line of code

[Kevin Buzzard]

We could make a big graph of what has been formalised, and a much bigger graph of what is claimed to be true in the informal literature, and then just give it to search experts and say "what do you need to make this good?" and they'll say "we need 1000 more theorems" and then I'll just start banging on on the interwebs or whatever about how we need important theorems in all of pure maths, and PhD students will randomly start formalising them and adding them to Hales' database. Why not? I can see this being a reality if this stuff catches on. At the minute it's too hard. But I think I see a way to make it not hard in the future. And these machine learning people are desperate for databases; they just use TPTP all the time, it seems to me. That's not mathematics -- that's just big Sudoku problems in some sense.

[Kevin Buzzard]

A separable Banach space is just a Banach space satisfying some predicate -- it would be easy to make if we had Banach spaces.

[Mario Carneiro]

Yes, but for every definition there are a hundred "obvious" theorems

[Mario Carneiro]

and mathematicians just expect those to be there by virtue of uttering the definition

[Kevin Buzzard]

Yeah but if we're just making a graph of theorems and not worrying about the proofs, it could be much quicker.

[Kevin Buzzard]

Hales does not want proofs.

[Adrian Chu]

Not just technical lemmas necessarily -- theorems announced in the literature whose proofs are not formalised. Once we have enough definitions with sufficiently good API then mathematicians will be able to start making their own definitions. At the minute it is really hard to make a meaty definition in Lean -- witness the fact that it just took a team of us months and months to do perfectoid spaces. But once we have a robust theory of "most normal things" it will get to the point where a mathematician can say "do you have separable Banach spaces? I want to state a result about them" and we say "well, we have Banach spaces, but nobody mentioned separable ones before, hang on, let me write one line of code, Ok now we have separable Banach spaces"

I think many mathematician probably won't bother to formalize proof, because I GUESS: even if the mathlib or lean language become mature enough, formalizing a PROOF will still be a few times more tedious/difficult than writing it into a paper. And just formalizing the statement of theorems/lemma are probably enough for a searching purpose?

[Kevin Buzzard]

Right.

[Kevin Buzzard]

Hales wants statements.

[Kevin Buzzard]

Fully formalised statements.

[Mario Carneiro]

But as we've seen, both in Fabs and the perfectoid project, stating a definition requires proving a theorem two or three abstractions below it

[Mario Carneiro]

and so the really complicated definitions need some fairly complicated theorems just to state

[Kevin Buzzard]

Right.

[Kevin Buzzard]

But after a while this bottoms out.

[Kevin Buzzard]

Here's something you maybe don't know about the perfectoid project.

[Kevin Buzzard]

perfectoid_space.lean is only a few lines long.

[Kevin Buzzard]

And that's because the definition is really easy, if you have basic topological ring stuff and the theory of adic spaces

[Kevin Buzzard]

Adic spaces were invented in 1992

[Kevin Buzzard]

All the work was implementing adic spaces.

[Kevin Buzzard]

If they'd been there already, perfectoid spaces would have taken 10 minutes.

[Mario Carneiro]

today's definitions depend on yesterday's theorems

[Kevin Buzzard]

Yes.

[Mario Carneiro]

can we get in front of that?

[Kevin Buzzard]

I think so

[Kevin Buzzard]

I think we can do that in my area of mathematics, algebraic number theory

[Kevin Buzzard]

I absolutely believe that now

[Kevin Buzzard]

But we are still a long way away.

[Kevin Buzzard]

And don't forget -- we can sorry the theorems

[Kevin Buzzard]

OK here's a challenge. Let's think about all the questions which the number theorists in my department are working on.

[Kevin Buzzard]

I think one interesting goal, for me at least, would be to try and formalise enough "basic" stuff so that I can state the theorems these people are proving.

[Mario Carneiro]

If you are willing to sorry all the theorems, I believe that you can formalize the statements of all those theorems in a week... if you are good at using lean, and you can transplant all their knowledge into your head

[Kevin Buzzard]

This is the sort of endeavour which ultimately will get people interested. It doesn't even have to be my department -- I can cheat and use people in UCL and KCL and cherry pick the easy ones

[Mario Carneiro]

the hard part, of course, is getting the lean-knowledge and number theory-knowledge in one place

[Kevin Buzzard]

If you are willing to sorry all the theorems, I believe that you can formalize the statements of all those theorems in a week... if you are good at using lean, and you can transplant all their knowledge into your head

I would like to think that I have a pretty good understanding of what pretty much all of the algebraic number theorists in London are working on.

[Kevin Buzzard]

But if we don't have algebraic closure yet -- you can't sorry a definition.

[Mario Carneiro]

You can axiomatize algebraic closure pretty easily

[Mario Carneiro]

don't let that stop you

[Kevin Buzzard]

https://www.imperial.ac.uk/media/imperial-college/research-centres-and-groups/cnrs-imperial/public/CNRS-UMI-Public-Lecture-30-May-2019.pdf

[Kevin Buzzard]

I'm preparing for this talk.

[Kevin Buzzard]

It's part of some two-day bash in London: https://www.imperial.ac.uk/abraham-de-moivre/seminars-and-events/UMI-workshop-2019/

[Kevin Buzzard]

I am basically trying to figure out whether my own wildly optimistic ideas are somehow reasonable enough to present to a room full of people some of whom will be very intelligent mathematicians whose expertise is in a completely different area of pure mathematics

[Andrew Ashworth]

I feel a little queasy inside every time I see an advert with "and in the future, AI will take our jobs, panic please"

[Andrew Ashworth]

people have way too much faith in the power of linear algebra...

[Kevin Buzzard]

Well then it is up to me to try and find exactly what is the reasonable thing to be said

[Kevin Buzzard]

because I am privileged enough to be able to get these kinds of gigs and I definitely don't want to come across as someone who is spouting BS.

[Kevin Buzzard]

I've already told the story here about how how I met someone in Obergurgl who says computers will be better than humans at maths within a decade.

[Kevin Buzzard]

I'm not sure I believe it. But I do believe that this sort of software will be able to change the way humans do mathematics within a decade and I might well say that in this lecture unless 10 people here on this chat start saying "no Kevin you moron, that is clearly not going to happen"

[Andrew Ashworth]

“It is difficult to get a man to understand something, when his salary depends on his not understanding it.”, hah

[Kevin Buzzard]

Computers beat humans at chess and we still have chess clubs.

[Kevin Buzzard]

In 10 years' time we'll certainly still have undergraduates to teach. And certainly most of those undergraduates are not going to go off to become pure math researchers

[Kevin Buzzard]

And it's the undergraduates tuition fees that are paying my salary, not any of this perfectoid space nonsense.

[Andrew Ashworth]

neural nets have been around for decades. what's new is that we finally have enough computer horsepower to make them useful for limited classes of problems like image recognition

[Kevin Buzzard]

But I need to be careful. I have been going round the UK preaching on "pure mathematics in crisis" and several people said to me that I was over-stating the case. As a consequence I had to think harder about this issue and talk to many people about how they felt about the fact that the community accepts proofs which are not at all well documented, and after a while I began to learn about how this was not a completely unreasonable point of view.

[Andrew Ashworth]

unfortunately the computer performance train has come screeching to a halt and the electrical engineering community is running around with their hats on fire

[Kevin Buzzard]

neural nets have been around for decades. what's new is that we finally have enough computer horsepower to make them useful for limited classes of problems like image recognition

The CS people I talked to at AITP have a different take on this.

[Andrew Ashworth]

if you asked the same people in the 70s, they would've said the same thing. then came the "great winter of AI"

[Andrew Ashworth]

it's even on wikipedia

[Andrew Ashworth]

https://en.wikipedia.org/wiki/AI_winter

[Kevin Buzzard]

The CS people at AITP were very keen to point out that 15 years ago everyone was going round saying that computer vision was impossible. Now everyone knows it's easy and we have forgotten that it was impossible, because we have self-driving cars.

[Kevin Buzzard]

We had a winter, and there are certainly people around who think that a new winter is coming.

[Kevin Buzzard]

But there are other people who are much more optimistic.

[Kevin Buzzard]

I am not going to be standing on that stage explaining that this is for sure how the future will be.

[Kevin Buzzard]

But it seems to me that the basic premise that Lean can help humans do mathematics because it can be used as a key component in a search algorithm and that we might be able to see the benefits within 10 years seems to me to be eminently reasonable and accessible with current technology

[Kevin Buzzard]

And if that's what I mean by "computers will change the way that humans do mathematics" then I think I am saying reasonable things, which most mathematicians are unaware of.

[Andrew Ashworth]

oh, of course, I'm also very enthusiastic about theorem assistants

[Andrew Ashworth]

I just happen to see a lot of AI hype because it's adjacent to my professional work

[Andrew Ashworth]

that's all I meant

[Kevin Buzzard]

And now there is the infinitely more optimistic scenario that computers will be winning the IMO within 10 years

[Kevin Buzzard]

and I have heard intelligent people suggest that this might be the case

[Kevin Buzzard]

and hence I am allowed to say "I have heard intelligent people suggest that this might be the case" but I need to be extremely careful not to say "This will be the case".

[Kevin Buzzard]

However, with search I feel like I am now in a position to begin to start saying "I believe that this will be the case"

[Kevin Buzzard]

And completely orthogonal to that, I am actively involved in trying to understand how Lean might be used in undergraduate education.

[Patrick Massot]

A separable Banach space is just a Banach space satisfying some predicate -- it would be easy to make if we had Banach spaces.

It's good that you wrote that. I went searching on GitHub to show you we do have Banach spaces. But I found out something went bad with https://github.com/leanprover-community/mathlib/pull/900 that I thought was merged two weeks ago. I'm trying again.

[Kevin Buzzard]

This is a completely different problem which presents a new set of challenges. @Patrick Massot it's about time we had a report on how your experience with teaching using Lean went.

[Kevin Buzzard]

I'd be particularly interested in a showcase of what you've managed to get your python code to do with commutative diagrams. Can I embed commutative diagrams in Lean comments and get something to render them yet?

[Kevin Buzzard]

But also I'd be interested to hear student reactions etc.

[Patrick Massot]

The commutative diagram question is easy. You can have a look at https://www.math.u-psud.fr/~pmassot/enseignement/math114/cours5.html

[Patrick Massot]

There are commutative diagrams near the middle

[Patrick Massot]

The Lean source for the first theorem where you see such a diagram is:

/- trad Théorème
Soit $X$ un ensemble muni d'une relation d'équivalence $∼$. Soit $f$ une fonction de $X$
dans un ensemble $Y$. Les conditions suivantes sont équivalentes :

1. il existe $\bar f : X/{∼} → Y$ telle que $\bar f ∘ π = f$
    ```cd
    X \dar[swap]{π} \rar{f} & Y \\
    X/{∼} \urar[dashed, swap]{\bar f} &
     ```
2. $∀ x, x' ∈ X,\; x ∼ x' ⇒ f(x) = f(x')$.
Lorsque les conditions du théorème sont vérifiées, on dit que « $f$ descend
au quotient ». La fonction $\bar f$ est alors unique, elle est appelée
« fonction induite par $f$ sur $X/{∼}$ ».
-/

[Patrick Massot]

The word "trad" on the first line means "traditional", it means there won't be any Lean code for that theorem

[Patrick Massot]

About the teaching report, I'll write that (in the dediced stream) in two weeks, after reading students evaluations and grading the exam.

[Kevin Buzzard]

I look forward to it! Thanks for the link! Am I supposed to be able to see the tactic state when I click on the small grey rectangles?

[Kevin Buzzard]

aah, it is under and not to the right?

[Alexander Kurz]

"And now there is the infinitely more optimistic scenario that computers will be winning the IMO within 10 years."

I am among those who are more skeptical. Recent advances in AI are due to machine learning which is very data hungry. Winning the IMO needs, afaics, to combine what ML is good at with using logic and learning from small number of examples ... this seems to be a challenge I have not seen yet much convincing progress (but I am not in ML or AI, so I might have missed it) ... any pointers welcome ... we would also need a natural language interface to theorem provers, is anyone working on this?

[Adrian Chu]

I'd wonder what language will be suitable for training machine learning to prove math theorem.

[Kevin Buzzard]

I am just quoting optimists I met at AITP

[Kevin Buzzard]

I think they were imagining the scenario where the questions were formalised in the language of the prover

[Olli]

are there people here who are working on applications of ML/AI into theorem proving?

[Patrick Massot]

http://aitp-conference.org/2019/

[Patrick Massot]

They are dreaming at least (and getting grant money of course, since they write AI on their grant application)

[Johan Commelin]

@Olli If you mean here in this chat... not that I'm aware of. Well, actually @Scott Morrison weren't you trying something with @Keeley Hoek

[Olli]

does anyone know if the recordings from the conference are watchable somewhere?

[Olli]

I'd be curious if anyone is applying methods from classical AI applied to games to theorem proving

[Olli]

just intuitively it feels like games and theorem proving are somewhat similar activities

[Olli]

quite surprised that my search on Google Scholar for "theorem proving" monte carlo tree search did not return anything directly relevant as far as I can tell

[Olli]

and no hits for "theorem proving" regret minimization"

[Kevin Buzzard]

There was someone from Deep Mind at AITP but they were not involved with the Alpha zero stuff. If a "game" is a 2 player thing then it seems to me that it's "puzzles" and theorem proving which are the most similar. One key difference is that maths is infinite whereas puzzles typically are not.

[Olli]

yes I agree that it's more like puzzle solving than playing a multiplayer game, but there is an area of study called Game Semantics that thinks of logic as a game played between the prover/computer/human vs. the omniscient disprover/environment/devil

[Olli]

furthermore, it seems like the ML people doing theorem proving are mostly focusing on trying to learn the activity of theorem proving by using theorems proved by humans as data, but one thing that I think TP and classical game type AI have in common, is that by defining the rules of the game, you can generate as much synthetic data as you please

[Patrick Massot]

I don't think it's easy to generate synthetic data here. A random sequence of math symbol is not good enough, even assuming it type checks

[Adrian Chu]

I don't get it, how is theorem proving like a game? Can you elaborate?

[Kevin Buzzard]

Theorem proving is like solving a Sudoku.

[Kevin Buzzard]

You have a precise list of rules, and then there are a bunch of levels and you have to solve the levels.

[Olli]

by game semantics you could think of sudoku as a game as well, although it's not as interesting as thinking of logic as a game

[Olli]

it's just a way of framing things slightly differently, but I wonder if this approach might be a useful one when it comes to AITP

[Olli]

so the idea is that the Prover plays against the Disprover, (or by Curry-Howard, the computer plays against the environment)

[Olli]

each logical operation is given meaning in this framing

[Johan Commelin]

@Olli Why don't you give it a shot?

[Olli]

@Johan Commelin I would like to, when I know a little bit more :)

[Olli]

http://www.csc.villanova.edu/~japaridz/CL/1.html#Subsection1a2

[Olli]

I came across this idea here, but Game Semantics is a wider field. one of its first big results was giving semantics to PCF (https://en.wikipedia.org/wiki/Programming_Computable_Functions)

[Olli]

and to linear logic before that

[Olli]

so I find it interesting, because it's a new perspective on the Curry-Howard isomorphism

[Adrian Chu]

how exactly is it related to Curry-Howard isomorphism??

[Olli]

you can think of a logical formula as a game, where each sub-expression represents a sub game-tree with the rules, where the play/proof advances play by play:

• the game is between the Verifier and Falsifier, and it ends when there are only atomic expressions left. If the expression is true then V wins, and if it is false then F wins.
• each logical operation is given meaning according to how it advances the game, so:
  • A ∧ B is a node in which the Falsifier gets to choose between A or B.
  • A ∨ B the same, but V gets to decide instead
  • ∀ (x : A), body the Falsifier chooses a value of A for which the play continues in body

etc. The game is winnable by the Verifier if he has a winning strategy against an omniscient opponent.

[Olli]

and you can have this same framing but where the game is played between the Computer and Environment instead, where Computer has the same role as the Verifier and Environment is the Falsifier

[Olli]

the proof / program is then viewed as a strategy in a game

[Adrian Chu]

is this a non-cooperative game in some sense?

[Olli]

yes, you could say it is zero-sum

[Johan Commelin]

@Olli for a lot of games, there is some sort of function that gives the winning chances for V (or F). I.e., given the current position in the game, who is likely to win.
Such a function seems to be a very important ingredient for AI approaches to games. Do you have a similar function for your game Logic?

[Olli]

oh yeah I forgot to mention the interpretation of ¬, which simply swaps the roles between Verifier/Computer and Falsifier/Environment

[Olli]

@Johan Commelin I have only just started reading about this area, so no I don't

[Olli]

I have thought about it, but I don't know how you would measure progress in a proof

[Olli]

I don't have a lot of experience with ITP or proving things in general, I've just messed around with Lean

[Adrian Chu]

can you give a very simple example, step by step, to illustrate ?

[Adrian Chu]

because this idea sound very interesting to me :)

[Alex J. Best]

You might be interested in HOList / DeepHol: https://sites.google.com/view/holist/home , see the ICML paper link there.

I wonder how tough it would be to make a lean backend for their code?

[Olli]

let me try to find an example from the Lean tutorial and see if I can write the game semantic interpretation for it

[Reid Barton]

GamePad (https://arxiv.org/abs/1806.00608) is another project similar to HOList I guess, but for Coq

[Kevin Buzzard]

I have thought about it, but I don't know how you would measure progress in a proof

This was pointed out to be a serious issue at AITP by one of the google speakers. It's hard to train an AI with such a poor definition of progress as the one we have: either "no, you have not done it, 0 points" or "yes, you have done it, all the points"

[Olli]

A really simple example:
(h : p ∧ q) : q ∧ p

So we are looking for a strategy for a game q ∧ p, where we have another game p ∧ q as a resource (hypothesis).

Since we are playing the and-game, the Falsifier gets to choose between p and q, and because we think of our strategy as a proof, then this means we have to describe what we would do in either case.

If F chooses p, then if we can provide a p then we win. We can get p by playing through our resource, where now the roles are reversed, which means we get to choose. Se we of course choose p and win this game. If F chooses q we similarly choose q from our hypotheses and thus we win the game regardless of what F chose.

Why are the roles reversed when we play in the resource game? Well I have to confess I am not sure if I know how to explain it, but I can make a few observations:

Classically A → B is the same as ¬A ∨ B, so an implies-game is a game where the Verifier gets to choose between playing the B-game or the reverse game of A.

So in our example if we instead are proving (p ∧ q) → (q ∧ p) which we kind of are, then this is a bigger game that is classically the ¬(p ∧ q) ∨ (q ∧ p) game, and because we are at the disjunction-node, the Verifier can choose to play the reverse game ¬(p ∧ q) which is just the game (p ∧ q) with the roles reversed. This means that eventhough we are dealing with an and-game, this time we the Verifier get to choose.

[Kevin Buzzard]

The holist link -- that's exactly the google people who were at AITP. https://arxiv.org/abs/1904.03241 . Szegedy was the guy who thinks maths will be done better by computers than by humans within 10 years. I talked to the authors of that project and they said that to a large extent their work was system-agnostic so could certainly be applied to Lean. They then asked me a couple of of technical questions about accessing Lean stuff programatically which I had no clue about.

[Adrian Chu]

@Olli can you please run through the steps of the example in your last paragraph ?

[Olli]

@Adrian Chu I don't quite understand the game semantics of implication, so it is possible that the last paragraph I wrote is just confusing things, like I said I only came upon this concept a few weeks ago so I don't know if I understand it well enough to explain it, I just thought of it might be relevant to AITP

[Olli]

although, ¬(p ∧ q) ∨ (q ∧ p) is a theorem, so there should be a way of explaining its proof as a strategy in a game

[Nicholas Scheel]

@Olli Yes, I think this is a simple manifestation of the duality of implication

[Nicholas Scheel]

Having hypotheses in scope is the "opposite" of having a goal to prove

[Nicholas Scheel]

In your game-theoretic example, this is shown in who gets to choose what

[Nicholas Scheel]

another way to see it is that q ∧ p is a stronger hypothesis but harder to prove than q ∨ p

[Olli]

yeah I was going to mention how in sequent calculus we can treat everything to the left of the turnstile as being implicitly in conjunction, whereas the right hand side is in disjunction, which I guess is another manifestation of what you said

[Johan Commelin]

@Olli Have you looked at tidy?

[Olli]

@Johan Commelin I know of it but don't know exactly how it works. I was learning Lean a while ago and just got through the TPIL book but then ended up a bit side-tracked with other things, but I have been meaning to come back to learn more

[Johan Commelin]

Search for the paper by Ganesalingam and Gowers. I think you may find it very interesting.

[Johan Commelin]

tidy roughly follows their strategy

[Olli]

thanks, I will check it out

[Jesse Michael Han]

You might be interested in HOList / DeepHol: https://sites.google.com/view/holist/home , see the ICML paper link there.

I wonder how tough it would be to make a lean backend for their code?

@Alex J. Best I will be working on that this summer, so we'll find out!

[Seul Baek]

I think Skolemization is a good example that is naturally understood in terms of game semantics

[Seul Baek]

A sentence ∀ x. ∃ y. φ[y] is satisfiable iff there exists a model such that, no matter which value the falsifier chooses for x, the verifier has a winning response in choosing the value of y

[Seul Baek]

This implies that ∀ x. φ[f(x)] is also satisfiable, since this sentence is still a win for the verifier if you choose the model in which f 'records' the said winning strategy

[Adrian Chu]

Can anyone give an overview of the current development of machine learning theorem proving? Like, what can we now achieve?

[Alex J. Best]

You might be interested in HOList / DeepHol: https://sites.google.com/view/holist/home , see the ICML paper link there.

I wonder how tough it would be to make a lean backend for their code?

Alex J. Best I will be working on that this summer, so we'll find out!

Oh great, hope it goes well. Sounds very cool.

[Andrew Ashworth]

If you like reading survey papers about AI, https://arxiv.org/abs/1801.00631 is quite good.

[Andrew Ashworth]

Well, I say "survey", but, it's more a general overview of issues with deep learning.

[Kevin Buzzard]

Can anyone give an overview of the current development of machine learning theorem proving? Like, what can we now achieve?

Take a look at the slides for the talks at AITP 2019, they're online. They will give you an idea of what people are working on.

[Kevin Buzzard]

http://aitp-conference.org/2019/

[Kevin Buzzard]

My cynical take on it is that the CS people are a million miles from proving anything that a mathematician might find interesting

[Kevin Buzzard]

I had some interesting email exchanges with Josef Urban around the time of the conference, I'll try to remember to summarise them when I'm near a computer -- they had some interesting links. A cynic's view -- the CS people like databases of theorems to train their AIs on and the only databases so far are the odd order work, flyspeck, TPTP, and the libraries for the theorem provers

[William Whistler]

I had some interesting email exchanges with Josef Urban around the time of the conference, I'll try to remember to summarise them when I'm near a computer

I'd be interested in this, if you're still willing!

[William Whistler]

(I've just been reading the TacticToe paper)

[Kevin Buzzard]

Here's a summary of some emails Josef Urban sent me around the time of AITP 2019.

[Kevin Buzzard]

TPTP (MPTP?) has some section about Bolzano Weierstrass. Here are some links he sent me about that although he said that more had happened since:

In Mizar: http://grid01.ciirc.cvut.cz/~mptp/7.13.01_4.181.1147/html/yellow19#T36

In FOL TPTP: https://github.com/JUrban/MPTP2078

Paper about verification using ATPs: https://doi.org/10.1007/978-3-540-75560-9_39

[Kevin Buzzard]

"We can't prove http://grid01.ciirc.cvut.cz/~mptp/7.13.01_4.181.1147/html/yellow19#T36 with ATPs, although it's probably close - we can prove e.g. T35. The really hard part would be proving e.g. T31 and http://grid01.ciirc.cvut.cz/~mptp/7.13.01_4.181.1147/html/yellow19#E35 . I don't think our AI/TP is there yet."

[Kevin Buzzard]

"I don't like that the ML and ATP people do not look at what they proved and only count numbers. They may miss some important insights. I do that often - to see what/how happens. See e.g. the examples of proved things in section 6 of https://doi.org/10.1007/s10817-014-9303-3 ."

[Kevin Buzzard]

"
News from the "State-of-the-art ATP over Large Math Corpora" department.

Enigma has just proved in 0.7s this problem: http://grid01.ciirc.cvut.cz/~mptp/7.13.01_4.181.1147/html/connsp_1#T14

It says that an image of a connected topological space under a continuous mapping is also a connected space.

The TPTP file is at http://grid01.ciirc.cvut.cz/~mptp/t14_connsp_1/t14_connsp_1 , the ATP proof at http://grid01.ciirc.cvut.cz/~mptp/t14_connsp_1/t14_connsp_1.out3 , and the ATP proof visualization at http://grid01.ciirc.cvut.cz/~mptp/t14_connsp_1/t14_connsp_1.svg . No other ATP can prove this in 60s, and we could not prove this before with many ATPs in 300s.

E was given 118 facts (145 clauses) about topology, connectedness, functions, relations, structures and sets, and it used 28 of them in the proof. The Mizar proof explicitly mentions 9 facts. The remaining 19 facts needed for the ATP proof are Mizar typing and "obvious" rules - like that every function is also a relation and that set intersection is commutative.

The E proof consists of about 108 clausal inferences. The proof search took 1177 nontrivial given clauses (1982 in total - included trivial and subsumed ones). And it generated 7k causes in total.

These are quite nice numbers: the proof is relatively long compared to the number of processed clauses, and the number of processed clauses is relatively high compared to the number of generated clauses.

I think Enigma is learning how to suppress too prolific inferences, and also how to routinely do the "mundane" mathematical stuff at the very bottom - like trivial operations over sets, relations and functions.

Examples like this could eventually go into some paper - or we could start a blog called "Advances of Automated Mathematicians" ;-).
"

[William Whistler]

That's useful information! Thanks, Kevin.