Hales' 2017 Big Proof talk

Stream: general

[Kevin Buzzard]

I'm giving a talk today at Inria and in the talk I mention Hales' July 2017 talk at the Big Proof Newton Institute workshop: https://www.newton.ac.uk/seminar/20170710100011001 (I always love the binary link, I think it means 10th July, 10am to 11am, room 1). It's worth investing an hour watching the video, but there's also a link to the slides on that page (although, like any good slide talk, the slides don't make sense by themselves, so you have to watch the video to hear the full story). I watched it again yesterday, to remind me of exactly what he had said and what the state of the art was in 2017. This was the talk that got me interested in Lean (I had never heard of Lean before this talk, but he mentions it in the answer to a question).

p11 of the slides talks about Lessons from the formalisation of Kepler, and one is:

Formalizers should be part of the tactical response teams that
routinely intervene in prominent, difficult, unpublished proofs.

I think that the work going on right now in the #condensed mathematics stream fits this description very well. We are formalising a prominent, difficult, unpublished result of Clausen and Scholze. Hales explicitly mentions the ABC conjecture on the next slide, and I had a discussion with Ivan Fesenko about whether this was feasible recently (I think the difficulty is getting someone to start doing it, I think a top-down formalisation would be one way to make progress).

Slide 32 talks about difficulties with Fabstracts and his attitude is "ignore them for now" -- my understanding of his point here is that we need to look at the greater goal of getting a deliverable to working mathematicians which they can actually understand. Right now we have difficulties with porting mathlib to Lean 4 but the overall goal of getting mathematicians interested in this area in general is greater than this obstruction which is why I am still highly motivated to continue working on mathematics in Lean 3. Someone in private conversations raised the possibility of just porting mathlib by hand, as did Daniel Selsam publically recently, and if this is what we ultimately have to do then I'm sure it will get done. This is going to be a hard problem but I don't think we should let it get in the way.

The final thing I want to flag is that on slide 34 Hales lists a bunch of things which would need to be done just to formalise statements in automorphic representation theory (the branch of number theory that Hales and I work in). I think that at the time that list just looked like a big joke to some people. But the first thing on the list is schemes and the last thing is perfectoid spaces, and we've shown that these things can be done. There is also measure theory, functional analysis, Galois theory, category theory, and we have many of the main definitions in mathlib now. There is also a bunch of stuff which we don't have but which I absolutely have one eye on. I think Hales' point with this slide was that even formalising part of number theory is going to be a huge amount of work, however I am not sure that even he would have envisaged that four years later one could look at his list and say "well a whole bunch of that stuff is either done, or could be done soon".

[Riccardo Brasca]

Can you give a link for today talk? Thank's!

[Kevin Buzzard]

I'm not sure it's public! It's also for computer scientists. http://68nqrt.inria.fr/index.html . Maybe the link just works?

[Kevin Buzzard]

It is a 30 minute seminar and then a 30 minute discussion.

[Riccardo Brasca]

It seems to work, thank you!

[Scott Morrison]

I enjoyed the talk.

[Scott Morrison]

I wonder if you actually failed to upset anyone. :-)

[Kevin Buzzard]

I tried really hard but I think my comments about Voevodsky could upset some people. I wanted to give the impression that you'll never attract most mathematicians unless you work classically, and basically I'm saying that Voevodsky's constructivism was a big mistake, but i know there are people who worship him

[Daniel Fabian]

Sorry I had to drop a bit early due a meeting. But I loved the talk ;-)

[Daniel Fabian]

@Kevin Buzzard are you aware of some typical theorems that don't work in a constructivist setting? (I mean not just painful to prove but known to not be provable)

[Kevin Buzzard]

The issue with this question is that it kind of assumes that the theorems I think about can even be stated in a constructivist setting. In algebraic geometry there is something called a scheme, which is a topological space which locally looks like an affine scheme, and an affine scheme is a topological space which is built from a commutative ring, and without LEM you cannot even prove that the thing you construct from the ring is a topological space, so in some sense an answer to your question is "every theorem about schemes". Here is a link to (something which unfolds to) a 7000 page pdf which has a few theorems about schemes: https://stacks.math.columbia.edu/ .

The answers that the constructivists give to this is "well you have to reformulate the statements so that they make sense construtively, you need to go and learn the theory of locales". But the moment I start talking about locales, I have lost all of the algebraic geometers in my department, who have never heard of locales. So for me this is not a satisfactory way to proceed.

[Daniel Fabian]

Nice, I hadn't realised you'd fail already at that level.

[Johan Commelin]

@Daniel Fabian Every ring has a maximal ideal. You need choice for that. And it's a fact that's used a number of times in getting commutative algebra of the ground (and hence algebraic geometry and a bunch of number theory)

[Damiano Testa]

Also,

• existence of algebraic closures,
• existence of bases of vector spaces,
• bipartite iff 2-colourable

are further examples of statements that are equivalent (I think) to the Axiom of choice.

On the other hand, "most" algebraic geometry used in practice is for schemes of finite type over ℤ (or ℚ, if you really need a field). In such cases, my guess is that many statements could be salvaged, but it would probably be hard, non-rewarding work.

[Johan Commelin]

@Damiano Testa We sure use algebraically closed fields a lot. But I guess we only really need $\mathbb C$ and $\bar\mathbb{F}_p$ most of the time...

[Damiano Testa]

I would go further and say that most of the times you use an a-priori-hard-to-specialize finite extension of the ground field. In many cases, you could probably work hard and figure out an extension that actually works, but... why?!?! :wink:

[Damiano Testa]

Something that took me a while to internalize is the difference between "closed under specialization" and "closed": it is tricky to come up with examples of "reasonable" properties of schemes that are closed under specialization, but not closed. Such properties would be good challenges for constructivism, I think.

[Damiano Testa]

For instance, proving the Noether-Lefschetz theorem for quartics in $\mathbb{P}^3_{\mathbb{C}}$ constructively could be a good test!

[Daniel Fabian]

@Johan Commelin thanks!

[David Wärn]

It's maybe worth pointing out that a lot of the strangeness of constructive mathematics comes from absence of LEM rather than choice. A pedestrian example of a theorem that's not valid constructively is "Z is a PID". The problem is that even if you have a decidable subset of Z, you can't tell if it has a non-zero element. Similarly with algebraic closures you can't tell if a polynomial is reducible or irreducible, so splitting fields are already problematic

[Anne Baanen]

Of course, the constructivist (me!) would say that the classical definition of PID misses the point, and ℤ is a perfectly fine Bézout wf_dvd_monoid.

[Scott Morrison]

@Anne Baanen, I'm curious to what you extent you think it would be viable for someone who cared about wf_dvd_monoids to contribute to refactoring mathlib "from the bottom" to introduce and use constructivist ideas. It would be essential that all the 90% that was still classical could stay essentially as it is (but that's okay, I presume, as PID -> wf_dvd_monoid). Presumably actually the question is about whether you think it would work from a community-interaction point of view.

[Anne Baanen]

I think making mathlib, as it stands right now, constructivist behind the scenes would require more than one person. There are quite a few fundamental definitions like finsupp, where treating them constructively was causing too much work for the classical side of things. If some of the technology improved (e.g. we wouldn't need to be so careful with decidable_eq), my hope is that making one definition constructive wouldn't break downstream usages (or at least, not as much as it does right now). In that case, people who care about constructivism don't make life worse for working classically, and I can see one or perhaps a pair of interested contributors making most of mathlib constructive.

One aspect of Lean that I think is an advantage for the constructivists, is that it is still ultimately based on type theory: there is a good notion of data in Lean, and you can point out instances where having access to this data is really useful for the working mathematician.

[Kevin Buzzard]

My arguments against constructivism are: (1) mathematicians in maths departments are brought up to think that constructivists are crazy, so even talking about constructivism involves some risk when it comes to being taken seriously by the mathematicians who matter (2) constructivism makes the library harder for mathematicians to use (c.f. Peter Nelson with his finset woes) (3) constructivists tend to overestimate the importance of constructivism in mathematics, perhaps due to their mathematical tastes not being aligned with what is actually going on in mathematics departments (i.e. a mismatch between what I think the word mathematics "means" and what a constructivist thinks it means).

Anecdotal evidence: when I read the odd order paper I was really turned off by the explanation of how they struggled to do representation theory because they didn't have access to the complex numbers, and simply could not understand what the point of working extra-hard to develop enough of a constructive theory of representation theory to push the arguments through. It was that, and the fact that they also highlighted their idea of defining a group hom from G to H as a partially defined map from some bigger group which contained G and H which just made me think that these people were crazy -- somehow they seemed to be investing a lot of time into issues which I felt should not be there in a proof system. However I really don't know how many other mathematicians would react the way I reacted to that paper. One can contrast that with what Patrick wrote in the perfectoid paper about extending continuous maps defined on dense subsets, and how he had the insight of not working with subsets at all but finding the correct abstraction and thus "beating Bourbaki" (a phrase he would not use himself, I know) where here he is proposing diverging from the standard literature but in a way which makes a lot of sense to me.

[Oliver Nash]

Isn't being constructive just a totally independent issue than being formal? You can do neither, either, or both. Why fight two wars at once? It's hard enough to be formal.

[Kevin Buzzard]

I thought formalising was a fun puzzle game, not a war :-)

[Oliver Nash]

It's an addiction! The war is getting others hooked :-)

[Anne Baanen]

Those three points are good ones, and IMO they are sufficient to show that we shouldn't replace mathlib with a purely constructive library. The way I approach constructivism is not as much a project to replace existing mathematics, but instead ask a new question, which I believe is interesting and can lead to useful insights: what do we need to do to make sense of these notions in a constructive/computational setting? And if the topic is not formalized at all, a classical formalization is much more useful to mathlib than an unfinished constructive formalization.

[Kevin Buzzard]

I think your approach is sensible and practical!

[David Wärn]

Oliver Nash said:

Isn't being constructive just a totally independent issue than being formal? You can do neither, either, or both. Why fight two wars at once? It's hard enough to be formal.

Sure you can do neither, either, or both (and I think it makes a lot of sense for mathlib to do one but generally not the other), but they're not totally separate issues. There's a lot of synergy between constructive mathematics and formal mathematics. If you want to prove things about your definitions, it helps if the computer can unfold your definitions, and this is easier if your definitions are constructive. I think there's even more synergy in univalent foundations, with its hProps. One of the fundamental obstructions to making mathlib constructive is the proof-irrelevant Prop. On the one hand it's very useful because you get lots of defeqs, on the other hand it's constructively problematic because you can't extract data from it.

[Joachim Hauge]

Oliver Nash said:

Isn't being constructive just a totally independent issue than being formal? You can do neither, either, or both. Why fight two wars at once? It's hard enough to be formal.

I guess they are not totally independent in the sense that if you go both formal and constructive then any natural number you define (like the rank of some elliptic curve over Q or the order of the torsion of some homotopy group) automatically comes with an algorithm to evaluate it. That algorithm probably won't be practical or efficient but there is some psychological comfort in having it.

[Kevin Buzzard]

But there is no known algorithm to compute the rank of an elliptic curve over Q, and yet I want to talk about it because I want to state BSD.

[Kevin Buzzard]

There are algorithms which work in most cases, but they rely on Sha being finite which is a big open problem.

[Kevin Buzzard]

Note that I do not feel at all psychologically uncomfortable about this fact :-)

[Joachim Hauge]

There is no algorithm that has been proven to be correct for all elliptic curves. But if you define a specific elliptic curve in a dependent type theory with canonicity then the rank of that specific elliptic curve (which is a closed term of N) necessarily comes with an algorithm to evaluate it.

[Kevin Buzzard]

This sounds to me like a massive warning sign to mathematicians -- "don't use dependent type theories with canonicity".

[Joachim Hauge]

A particular strain of mathematicians has come to dominate the funding agencies and universities but I'm not sure what the reasons for that are. It would seem the society at large doesn't care either way.

[Kevin Buzzard]

In fact I am really confused by what you are saying. I can just write down $y^2=x^3+38756382756386x+23478368756345$ and it might be the case that humanity cannot prove that there is an algorithm which is guaranteed to terminate to compute the rank of this curve. Yet I want to be able to state BSD in Lean, because if I cannot then the particular strain of mathematicians who have come to dominate the funding agencies and universities, i.e. precisely the people that it is absolutely crucially important that we as a community appeal to if we want this area to grow, will think our prover is useless.

[Kevin Buzzard]

Oh OK I am unconfused. The point is that the definition of rank is this: "I can write down a concrete computable Q-vector space. I can write down a noncomputable predicate on this which cuts out a subspace. The rank is the dimension of this subspace".

[Kevin Buzzard]

Mathematicians decided 100 years ago that if they allowed this definition then mathematics would grow much faster, and now there's no going back.

[Kevin Buzzard]

This case is particularly subtle, because there is actually also an algorithm which should in theory define a computable predicate which cuts out the same subspace, but nobody can prove that it terminates in general (although it always terminated whenever anyone ran it on a concrete elliptic curve).

[Mario Carneiro]

If you want to prove things about your definitions, it helps if the computer can unfold your definitions, and this is easier if your definitions are constructive.

I don't really buy this argument anymore. "Constructive" means "computable" only in the barest possible sense; if you actually really care about computation, the stuff intuitionistic mathematics gives you is not very useful. Put another way, constructive mathematics tries to be both mathematics and computation, and ends up being a poor approximation of both. What's more, it turns out that when reasoning about algorithms there isn't any particular reason to be constructive in your logic; you can still prove asymptotic bounds on programs and all the rest.

[Mario Carneiro]

One of the fundamental obstructions to making mathlib constructive is the proof-irrelevant Prop. On the one hand it's very useful because you get lots of defeqs, on the other hand it's constructively problematic because you can't extract data from it.

I wouldn't call this a fundamental obstruction. The basic idea is that if you want to extract data from something, put it in Type, otherwise put it in Prop. You can still do many of the hProp tricks in Type, for example trunc is the (computable!) propositional truncation, and you can eliminate from it to any type that is a subsingleton.

[Mario Carneiro]

Most constructions that we can actually reasonably compute are in the correct universes for doing so. If not, there would be a lot more noncomputable stuff than there currently is

[Mario Carneiro]

There are a few notable exceptions, like finsupp, polynomial and real, where we could be computable and made a conscious decision not to be in order to make the maths smoother, but in all cases there is actually some subtlety to picking an appropriate data representation to be not just computable but also computationally efficient, and the plan is to make computational analogues of these types if and when they get used for some algorithm, so that they can be appropriately tailored to that use-case.

[Mario Carneiro]

A good recent example is from the itauto decision procedure I PR'd. This starts with a definition of an inductive type prop representing intuitionistic propositions. Even though lean's Prop is "not computable", that didn't prevent me from writing a program that computes with elements of Prop, because I can just reflect into an inductive type tailored to the purpose at hand.

[Mario Carneiro]

norm_num works the same way. Even though equality on real is "not computable":

import data.real.basic
example : (2 + 5 / 2 : ℝ) = 9 / 2 := by norm_num
example : (2 + 5 / 2 : ℝ) ≠ 0 := by norm_num

It seems "not computable" doesn't actually mean what it sounds

[Sebastien Gouezel]

By the way, would there be a conceptual problem in making polynomials irreducible? Currently, they are not, and this led to some difficulties in #7084 (big rfl or convert that are unreasonably slow).

[Johan Commelin]

I think @Scott Morrison has tried this, but it caused a lot of breakage.

[Scott Morrison]

Gabriel has done some very helpful work in this direction too.

[Scott Morrison]

I think there have been several rounds of: 1) make polynomial irreducible 2) fix some breakages 3) revert it to semireducible because you didn't fix everything 4) PR the fixes.

[Scott Morrison]

It would be lovely to be able to omit step 3)!

[David Wärn]

Kevin Buzzard said:

This sounds to me like a massive warning sign to mathematicians -- "don't use dependent type theories with canonicity".

You can still define noncomputable numbers like the rank of an elliptic curve in such a system. It just won't be a natural number, but some sort of generalised natural number -- "bounded initial segment of N", or something like this. You might not like this, I'm just trying to say that it's possible to express these things constructively

[Gabriel Ebner]

The double-negation fragment of constructive mathematics is indeed the most natural one. :rofl:

[David Wärn]

What's more, it turns out that when reasoning about algorithms there isn't any particular reason to be constructive in your logic; you can still prove asymptotic bounds on programs and all the rest.

Sure. But there is a reason to be constructive in your logic if you want to extract data from your proofs. If you want to prove that f is bijective and injective, and then get a computable inverse from this proof, then your logic had better be constructive.

[David Wärn]

I wouldn't call this a fundamental obstruction. The basic idea is that if you want to extract data from something, put it in Type, otherwise put it in Prop. You can still do many of the hProp tricks in Type, for example trunc is the (computable!) propositional truncation, and you can eliminate from it to any type that is a subsingleton.

It's not a fundamental obstruction in the sense that you can do constructive reasoning in Lean using trunc. But mathlib doesn't use trunc very much (for good reason!), so using mathlib constructively becomes awkward. (And subsingleton elimination is more powerful in UF than in Lean since you get more subsingletons, like "the type of initial objects in a univalent category")

[David Wärn]

Note I was only trying to make the weak claim that constructivism and formal mathematics have some synergy, not that constructive mathematics is easier to formalise. It seems to me that using norm_num to compute on ℝ just moves the problem of "making arithemtic computable" from definitions to lemmas and tactics. I'm not saying there's anything wrong with this, but at the end of the day you're still thinking about similar problems as constructive mathematicians, i.e. "how to make maths compute".

[David Wärn]

Of course intuitionistic logic sometimes gives you algorithms that are worthless in practice. But there's also nothing stopping you from defining efficient algorithms constructively

[Gabriel Ebner]

David Wärn said:

[...] using norm_num to compute on ℝ just moves the problem of "making arithemtic computable" from definitions to lemmas and tactics.

Isn't that the only possible way? I.e., there is no way to make (=) : ℝ → ℝ → bool computable, but norm_num can still compute many useful real numbers.

[David Wärn]

Sure. I'm out of my depth here, but I'd expect to be able to prove certain other things about real numbers, like sin.real 0.1 > 0, 'by computation', assuming sin.real were sufficiently computable

[David Wärn]

I mean, with another model of the reals, we could have a computable function that takes a real number and gives you a rational approximation with error at most 0.01 (possibly wrapped in trunc). As I understand, this could in principle be done by a future version of norm_num, but the work has not yet been done?

[Kevin Buzzard]

Yeah, I guess that would require a whole lot of work, one would need theorems of the form "if x is in this box with rational endpoints then sin(x) is in that box with rational endpoints, and if we make the first box smaller then the second box gets smaller". I suspect the reason this sort of thing isn't happening is that you can formalise a huge amount of mathematics without ever even caring whether sin(0.1) is positive or negative, and the current driving force in mathlib is somehow people doing other stuff. My guess is that if you were to start prodding the Coq people you'd find a ton of stuff done in this direction.

[Johan Commelin]

Right, we have a little bit in this direction. Just enough to define real.pi. (And we can even compute the first 5 digits or so :shock: :open_mouth:)
But I don't think that I know of any other proof where you wan't to plug some x into real.sin where x isn't "special".

[Kevin Buzzard]

My guess is that this stuff will happen organically when it's needed. Right now we are romping ahead with theorems of Scholze involving real numbers without ever actually mentioning an explicit real number at all. The only reason we can evaluate pi to even one decimal place was that we decided it would be a fun thing to do on pi day two years ago :-) But I would imagine that there are people here who might well one day need this kind of stuff. Growth of mathlib can often be motivated by people having lofty goals and then focussing on what needs to be done next in order to attain them. Right now I don't see a lofty goal which needs to know whether sin(0.1) is positive or negative, but one I guess could imagine it appearing in the future.

[Mario Carneiro]

David Wärn said:

I mean, with another model of the reals, we could have a computable function that takes a real number and gives you a rational approximation with error at most 0.01 (possibly wrapped in trunc). As I understand, this could in principle be done by a future version of norm_num, but the work has not yet been done?

Actually this is impossible, at least with cauchy representation, even if you use efficiently converging cauchy sequences. Given a particular cauchy sequence, you can get an arbitrarily good rational approximation computably, but once you take the quotient, different cauchy sequences will give different approximate results and even though any of them would be "fine" you still can't get a particular answer out.

[David Wärn]

This is solved by wrapping result in trunc right?

[Mario Carneiro]

However this can be done by norm_num, because it doesn't work on the actual type real as understood by constructivists, it works on representations of real numbers in a more explicitly computable subset such as algebraic numbers

[Mario Carneiro]

Wrapping the result in trunc means you never get an answer to the question though

[Mario Carneiro]

it's possible to give an approximate lt function on real which outputs trunc bool but what good is that?

[Gabriel Ebner]

sin(0.1) is positive or negative

This particular instance is actually very easy to prove. But it would of course be great to have interval arithmetic (or sth similar) in mathlib.

example : 0 < sin 0.1 := sin_pos_of_pos_of_le_one (by norm_num) (by norm_num)

[Bryan Gin-ge Chen]

Johan Commelin said:

Right, we have a little bit in this direction. Just enough to define real.pi. (And we can even compute the first 5 digits or so :shock: :open_mouth:)
But I don't think that I know of any other proof where you wan't to plug some x into real.sin where x isn't "special".

I doubt this is something we can target in the near future (unless we manage to attract some numerical analysts?), but I could imagine a program in Lean N that generates a plot of sin with an accompanying proof of correctness, e.g. that the black pixels are all "close" to actual values. (see also the Lean 4 raytracers.)

[Kevin Buzzard]

In Coq they have it already: https://coq.discourse.group/t/interval-4-2-now-with-plotting/1248

[Mario Carneiro]

I don't know how to prove 0 < sin 0.1 in computable real arithmetic the constructive way though, because the type of < doesn't really admit a total function

[Mario Carneiro]

It's possible to prove it with a proof, but not some #eval thing

[Kevin Buzzard]

(although I'm confused about the floor function graph in that Coq link because for sure there's a lot of points on that staircase graph which are provably nowhere near actual values)

[David Wärn]

Of course we can't make < computable. But you could have a computable approx : Π (x : ℝ), trunc { y : ℚ // abs (x - y) < 0.01 }. Then it's easy to prove concrete inequalities where the gap is large enough: just compare the two approximations

[Gabriel Ebner]

How do you prove that the gap is large enough?

[David Wärn]

What do you mean? Given a particular inequality, like sin (e + pi) < -0.4, you'd be able to prove it just by comparing approximations. AFAICT this is currently tricky in Lean only because you don't have access to rational approximations

[Mario Carneiro]

Incidentally, it's easy to prove in mathlib that 0 < sin 0.1, since we know sin is positive on (0, pi) and 0 < 0.1 < 3 < pi can be verified by norm_num and a lemma about pi

[Johan Commelin]

Gabriel Ebner said:

sin(0.1) is positive or negative

This particular instance is actually very easy to prove. But it would of course be great to have interval arithmetic (or sth similar) in mathlib.

example : 0 < sin 0.1 := sin_pos_of_pos_of_le_one (by norm_num) (by norm_num)

@Mario Carneiro :up:

[Mario Carneiro]

@David Wärn That method works well if you have a particular cauchy sequence to work with, and this is what actual "exact real arithmetic" packages in languages like C++ or Haskell do. But if you drink the intuitionist coolaid then you will want to take a quotient of those cauchy sequences so that you have the "real reals" instead of just some surjective cover with too much data in it, and once you do that you lose all ability to distinguish anything from anything else

[Gabriel Ebner]

David Wärn said:

What do you mean? Given a particular inequality, like sin (e + pi) < -0.4, you'd be able to prove it just by comparing approximations. AFAICT this is currently tricky in Lean only because you don't have access to rational approximations

But the trunc representation doesn't give you that. You still need to show that the approximate intervals don't overlap.

[David Wärn]

Well the approximations are sufficiently far apart, so the original numbers must be too

[Gabriel Ebner]

Yes, that's clear. But you can't do that with trunc { y : ℚ // abs (x - y) < 0.01 }. If you define a function on the truncation, you need to prove that it is constant, i.e., it returns the same value for every approximation. And that's only true if the intervals don't overlap.

[David Wärn]

Right. This wouldn't give you a total computable <, but it would help you write tactics to prove particular inequalities

[Mario Carneiro]

For a simpler example, let's say we want to prove 0 < e given an algorithm for e. We can build trunc {q | abs (e - q) < 1}, and if we run it let's say we get 2, but it's behind the quotient so we aren't allowed to tell the difference between this and 2.5 and other numbers that we can't be sure about. Now if we see 2 we can conclude that any other number in the equivalence class is within 1 of 2 and therefore e is positive. But we don't know that we can only get 2. We need to know that all values within 1 of 2 have this property, and so we aren't sure that 1.5 isn't in the equivalence class too, or 1, or 0.5 or 0 where we're definitely hosed. We want a function that says "yes", "no" or "inconclusive", but the line between "yes" and "inconclusive" is itself fuzzy and basically makes everything "inconclusive"

[David Wärn]

Isn't this solved by tactics? E.g. can't I write a tactic which takes an assumption trunc.mk a : trunc A in context and replaces it with a : A?

[Mario Carneiro]

Yes, that's the norm_num way. Forget about computing in the logic, and look at the terms that were written down instead

[Mario Carneiro]

when you step up a meta-level everything becomes computable because it's all lambda calculus

[Mario Carneiro]

But my point is that once you take that step, it becomes utterly irrelevant whether the object language has choice or LEM or uses constructive logic or can run proofs, because you are looking at the proofs and can compute whatever you want. Isabelle uses a code generation scheme along these lines and the idea that you need constructive mathematics to be able to run functions from the logic is very foreign to them

[David Wärn]

Sure. But if your definitions aren't constructive from the beginning, and you want to compute with them, then you need to add lemmas and tactics to compute with them. Whereas if you had a computable model of say the reals from the beginning, then you'd get computable rational approximations for free

[David Wärn]

Mario Carneiro said:

David Wärn That method works well if you have a particular cauchy sequence to work with, and this is what actual "exact real arithmetic" packages in languages like C++ or Haskell do. But if you drink the intuitionist coolaid then you will want to take a quotient of those cauchy sequences so that you have the "real reals" instead of just some surjective cover with too much data in it, and once you do that you lose all ability to distinguish anything from anything else

I don't understand what you mean by this. If you have a setoid version of the reals, with no quotienting, then you don't even need to wrap your approximations in trunc. But if your reals are equivalence classes of Cauchy sequences (or a recursive HIT like in the HoTT book), can't you still get approximations wrapped in trunc?

[Mario Carneiro]

Yes, but an approximation wrapped in trunc cannot be printed, because the printing does not satisfy the quotient property

[Mario Carneiro]

nor can it be compared to a given rational, unless you already know the answer in advance

[Mario Carneiro]

any function defined out of the trunc has to be locally constant as Gabriel said, and all such functions are trivial

[David Wärn]

But at least you could feed it to a tactic to do things like

example : sin (e + pi) < -0.4 := by rat_approx

[Mario Carneiro]

Yes, but you don't need computable reals to do that

[Mario Carneiro]

You can implement exactly the same rat_approx tactic whether real is constructive or nonconstructive

[David Wärn]

Sure

[David Wärn]

I never meant to argue against this

[Mario Carneiro]

My view is that this rat_approx approach is the right one, and the intuitionistic constructive reals thing doesn't actually solve the problems it set out to do

[David Wärn]

I'm just saying that you get more for free if your definitions are constructive. You initially save effort working nonconstructively, but then you still need to write code to compute with things. (I'm not saying either approach is better overall)

[Mario Carneiro]

If I want to compute pi, I will use some crazy formula with good convergence. That doesn't mean the abstract definition of pi needs to be that. I certainly wouldn't want to be messing with a formula about arctan when I still haven't proved that pi exists. These are different things for different purposes, so defining things twice is a strength, not a weakness

[Mario Carneiro]

Sometimes, the mathematical definition is also good computationally. Maybe list.map is an example. But these are in the minority - even list.map has to sacrifice a lot of performance because it works on linked lists instead of arrays. Most algorithms are very different from the abstract concepts they compute

[Joachim Hauge]

Mario Carneiro said:

If I want to compute pi, I will use some crazy formula with good convergence. That doesn't mean the abstract definition of pi needs to be that. I certainly wouldn't want to be messing with a formula about arctan when I still haven't proved that pi exists. These are different things for different purposes, so defining things twice is a strength, not a weakness

I think the issue here is that in intensional type theory you can have non-equal real numbers with the same sequence of digits. So when you are talking about "pi" you are really talking about several different objects.

[Johan Commelin]

@Joachim Hauge That doesn't seem "practical or efficient" and neither do I get any "psychological comfort in having it".

[Johan Commelin]

So I'm glad that there is just one real.pi in mathlib, and that we can write a tactic to compute it's digits.

[Kevin Buzzard]

Right, so this idea about different reals with the same digits might be interesting to some foundational people but it is also a massive red flag when it comes to attracting conventional mathematicians to proof assistants (which is my ultimate goal and the motivation behind a lot of my work). What you describe might lead to foundational questions of interest to some people but it is not the model of mathematics which is in the head of the important mathematicians so it should not be the direction of travel for mathlib if we want to further penetrate the market

[David Wärn]

This is not about constructivism. It's true that there are (also in Lean) terms like 0 + pi and pi that represent the same real number but are not defeq. I guess in some sense this is due to the fact that they represent different ways of computing pi. But it doesn't matter much to theorem proving, since they're still (propositionally) equal. (You can construct other computable real numbers which are "actually" equal but not provably equal, by Gödel, but that's really beside the point.) The equality 0+pi = pi is perfectly constructive. Constructive reals (like the HIT reals) have exactly the same extensionality as you'd expect

[Mario Carneiro]

I guess the "equal" that Joachim Hauge mentions is what we would call defeq, and following Kevin's remarks this is exactly why I consider defeq a scourge and ITT misguided for making me care about a manifestly non-mathematical relation

[Mario Carneiro]

But, @David Wärn, the equality 0+pi = pi won't necessarily be an equality if you leave the reals unquotiented (actually in that particular example it probably is, but there are minor variations that won't be like (2 * pi) / 2). So you get stuck in this middle ground where either you have the desirable mathematical properties (with the quotient) or the computational properties (without the quotient) but not both.

[David Wärn]

I claim that you still retain some good computational properties with the quotient. You don't get total computable (=) or (<), but that's unavoidable and unrelated to the quotient. What you do get is computable trunc-wrapped rational approximations. Given this, writing a tactic to prove inequalities in the reals is trivial. Whereas with mathlib's noncomputable reals, proving sin(e + pi) < -0.4, which should just be a matter of unfolding definitions, is not that easy.

[Mario Carneiro]

It is possible to implement a prover for sin(e + pi) < -0.4 by associating computational methods to sin, e, pi and +. This is essentially the same as what you would need to do with a computable real definition of sin, e, pi, etc except that you would also have to prove equivalence of these computations to the real thing. The computable real approach skips this step, but instead you would need to work with this computational method when proving that sin pi = 0 and all those other pure maths facts

[Kevin Buzzard]

@Joachim Hauge Mario has now explained what I presume you mean, but for mathematicians there is only one kind of equality. The reason the natural number game makes sense to mathematicians is that I explicitly had to "disable" checking for definitional equality so that mathematicians could not tell the difference between the defeq n+0=n and the theorem 0+n=n. No mathematician would accept the idea that these two kinds of equalities are distinct because we think of mathematics in a very symmetric way and breaking the symmetry is confusing to us. We have one equality to rule them all, namely mathematical equality -- the idea that two things are "the same". We have done well for centuries never going into any further details and these things need to shielded from mathematicians. In NNG n+0=n is proved with rw add_zero and not rfl, and I think this is key to the accessibility for mathematicians. Our instinct is to prove equalities by rewriting rather than unfolding.

[Sebastien Gouezel]

For #7084, I had to modify the definition of power, so that x ^ 0 is not defeq to 1, and x ^ n.succ is not defeq to x * x^n any more. This means a lot of proofs broke because they were abusing these definitional equalities, and instead I had to rw [pow_zero] or rw [pow_succ] a lot. I feel this is really for the better, because now the proofs are both more readable and more robust. I came slowly to the conclusion that the only place where defeq really matters is not in userland, but in instanceland where the kernel is checking things and you don't have control on what it is doing.

[Scott Morrison]

I think it's a bit unfair to say for mathematicians there is only one kind of equality. As well as the "usual" one, once you receive your licence to use the word "canonical", you can arbitrarily use the = symbol instead of ≅. :shrug:

[Scott Morrison]

defeq:

The version I heard is that Pauli was lecturing, and he said "this is obvious". A student raises his hand and says "sorry professor, I don't think that is obvious". Pauli stares at the board, back at the students. He thinks for a bit. He starts pacing in front of the class, thinking. He looks back at the board. Eventually he leaves the room, comes back 20 minutes later and says "I've thought about it and yes, it is obvious".

That's an awesome super power to have, but not one that really scales well.

[Sebastien Gouezel]

I had never thought of Pauli in this story as the kernel checking a heavy rfl, but this is exactly it!

[Sebastien Gouezel]

Scott Morrison said:

I think there have been several rounds of: 1) make polynomial irreducible 2) fix some breakages 3) revert it to semireducible because you didn't fix everything 4) PR the fixes.

#7421

[Johan Commelin]

@Sebastien Gouezel Wow! You really are on a rampage!

[Sebastien Gouezel]

Effective procrastination :-)

[Eric Wieser]

It worries me a little that this ends up adding 500 lines of what are essentially repeated proofs, and makes translating proofs from finsupp to polynomial (an activity which the original problem is partly due to the neglect of) harder. Is there any way we can better handle this with automation?

[Eric Wieser]

And unrelatedly, I assume the follow-up would be to do this to mv_polynomial too?

[Anne Baanen]

Thank you for the hard work! I don't think the translation from finsupp to polynomial becomes much harder, since we still have the isomorphism between the two, to_finsupp_iso. (Indeed, I suspect the total amount of changes could have been smaller by using to_finsupp_iso rather than re-proving the existing results, although I have not tried doing so yet.)

[Sebastien Gouezel]

In fact, there isn't a lot of proof repetition. Most of the additional code is to set up all the operations on polynomial R by lifting to finsupp, then declaring everything irreducible and registering the basic properties. Once this is done, all proofs are essentially straightforward (and when they're not one-liners we can either lift things to finsupp or use to_finsupp_iso. Another source of addition is that several concepts were only defined for finsupp, but used liberally for polynomials (like erase or frange), so one has to register again the definitions and the basic properties.

[Sebastien Gouezel]

The only real pain I encountered is that, after the refactoring, Lean can not at all compute with polynomials (before, it could compute their support), so 0.coeff n is not definitionally equal to 0, and 0.degree, 0.nat_degree, 0.leading_coeff and so on have to be handled by rewrites instead of rfl. Once the basic few files had been done, this was essentially the only thing that needed fixing all over the library.

[Kevin Buzzard]

This sort of thing is what makes computer scientists shudder, and I think that this is a good reason for trying it, because it is trying to set up a theory in a way which is not at all intuitive for the kind of people who have been setting up theories of polynomials before. Mathematicians prove n+0=n by a rewrite in the natural number game because 0+n=n needs a rewrite and the proof of n+0=n feels like it should be the same because of our internal symmetry

[Eric Wieser]

This is all because lean doesn't consider structures with defeq members as defeq, right?

[Eric Wieser]

(except in typeclass inference where it knows to try unpacking fields?)

[Gabriel Ebner]

Sebastien Gouezel said:

The only real pain I encountered is that, after the refactoring, Lean can not at all compute with polynomials (before, it could compute their support), so 0.coeff n is not definitionally equal to 0, [...]

If you want 0.coeff n to reduce to 0, then you shouldn't mark it as irreducible.