My last post was, amongst other things, a challenge for the community behind every modern computer proof verification system to start formalising “proper mathematics”. This term has some problems, so how about the equally vague but perhaps less offensive “fashionable mathematics”. What mathematics is fashionable? Just take a look at the work of the recent Fields Medallists. That’s a pretty good way of telling.
But fortunately, unlike many other fashions, “fashionable mathematics” is not controlled by the whim of big companies or some cabal. Fashionable mathematics is mathematics which justifies itself by its ability to answer questions which have been previously deemed interesting or important. Peter Scholze’s definition of a perfectoid space opened a door. In the last ten years, perfectoid spaces have been used to prove new cases of the monodromy-weight conjecture, to prove the direct summand conjecture, to give a new proof of purity for flat cohomology, a strengthened version of the almost purity theorem and so on (and I didn’t even mention applications to the Langlands philosophy). These are results whose statements do not mention perfectoid spaces, and some have been open for decades. This is what makes this kind of mathematics fashionable — it is giving my community new insights.
Each formal proof verification system (Lean, Coq, Isabelle/HOL, UniMath, all of the others) has its own community, and it is surely in the interests of their members to see their communities grow. These systems are all claiming to do mathematics, as well as other things too (program verification, research into higher topos theory and higher type theory etc). But two things have become clear to me over the last two years or so:
- There is a large community of mathematicians out there who simply cannot join these communities because the learning curve is too high and much of the documentation is written for computer scientists.
- Even if a mathematician battles their way into one of these communities, there is a risk that they will not find the kind of mathematics which they are being taught, or teaching, in their own department, and there is a very big risk that they will not find much fashionable mathematics.
My explicit question to all the people in these formal proof verification communities is: what are you doing about this?
Now you — I don’t mean an individual — I mean you as a community of Coq users or Isabelle/HOL users or UniMath users or whatever — you might decide that these things are not important, and hence the answer is that you are doing nothing. You might simply decide to reject the idea that formalising fashionable mathematics is important. And this is fine. But, in return, don’t expect us to come and join your community. You might not want us! This is fine! But we represent true potential for growth.
What some of us mathematicians believe is that at some point in the future, it’s not completely out of the question that one or more of these systems actually start becoming useful for our research. But what is completely clear is that if none of these systems actually know what the class group of a number field is then this is a rock solid proof that the systems cannot currently be used to help us prove even basic results about class groups of number fields, let alone new results.
Univalent people.
I have had extensive conversations with people interested in univalent mathematics. I initially rejected univalent mathematics completely because its “abuse” (as I initially saw it) of the equality symbol was so obscene to me. Mathematicians use the equality symbol (i.e. 
What I have noticed amongst the univalent people is that, more than any of the other communities I’ve run into, they really do not seem to care about doing “fashionable mathematics”. I would love to be spammed with comments telling me that I was wrong about this. But my impression is that there are a whole bunch of interesting type theory questions raised by the univalence axiom, and that these foundational questions are what the community is on the whole interested in. I have asked lots of univalent people how it could possibly be the case that Voevodsky, someone who made their name by discovering a homotopy theory for schemes, could spend 15 years working in univalent type theory and still not have a definition of a scheme at the end of it. It has been explained to me, on more than one occasion, that Voevodsky’s interests changed. This is fine. But I still want the schemes. Here is a message for you univalent people — if you do not actually build some fashionable mathematics at some point, then we will not come in our masses. Where is the definition of a scheme? Where is the proof that the class group of a number field is finite? Where are number fields, for that matter? Can you really show me that it does not matter that all number fields are countably infinite, and hence biject with each other, and hence are equal, in your system? I know that’s not how it works and there’s more to it than that. But I don’t want to hear protestations, I want to see the code. UniMath, Arend, any system you like. I know you’re good at higher topos theory but where is the arithmetic? Where is quadratic reciprocity?
Coq users
Coq users: you have a mature system which has been around for decades and is tried and tested. You have formalised several very difficult proofs about undergraduate-level mathematical objects such as planar graphs and finite groups. You have done lots of computer science things which I do not understand too. But where are the MSc level mathematical objects? Where are the schemes? Coq is French! Schemes are French too! It’s a match made in heaven! Where are the statements of local and global class field theory? Assia Mahboubi is someone who is actually doing mathematics in Coq which “proper mathematicians” are interested in. She cannot do it alone! Where is the manual which tells mathematicians who have no idea what a type is but know what a Noetherian ring is, where to start? What if an undergraduate wants to try formalising the Hilbert basis theorem? What do they do? Ask on the mailing list? You know that undergraduates don’t actually use email any more, right? I am told by my teenage children that email is for old people. Where is the way in for us? [Note added 14th Feb: thanks to Théo Zimmermann for pointing out to me on Twitter that Coq has a Discourse forum. Young people wanting to learn Coq — try asking some beginner questions there. Ask how to make class groups of number fields! Let’s get more serious mathematics done in Coq! It’s an extremely powerful system! ]
Isabelle/HOL users
Isabelle/HOL: Manuel Eberl is tirelessly generating 20th century analysis and analytic number theory. This is a highly respectable thing to do — he is planting the seeds. He is doing the basics. He cannot do it alone! Furthermore, HOL has no dependent types. Does this mean that there are entire areas of mathematics which are off limits to his system? I conjecture yes. Prove me wrong. Can you define the Picard group of a scheme in Isabelle/HOL? I am not sure that it is even possible to write this code in Isabelle/HOL in such a way that it will run in finite time, because you have to take a tensor product of sheaves of modules to define the multiplication, and a sheaf is a dependent type, and your clever HOL workarounds will not let you use typeclasses to define module structures on the modules which are values of the sheaves. So how will you do the tensor product? I don’t know. Does anyone know? Is this actually an interesting open research problem? Picard groups of schemes are used all over the place in the proof of Fermat’s Last Theorem. They are basic objects for a “proper mathematician”. What can Isabelle/HOL actually do before it breaks? Nobody knows. But what frustrates me is that nobody in the Isabelle/HOL community seems to care. Larry Paulson says that it’s easy to understand: different kinds of maths work best in different systems, and so you might want to choose the system depending on the maths you want to do. But do you people want to attract “working mathematicians”? Then where are the schemes? Can your system even do schemes? I don’t know. Does anyone know? If it cannot then this would be very valuable to know because it will help mathematician early adopters to make an informed decision about which system to use. [Notes added Feb 14th: Josh Chen told me on Twitter that Isabelle has a Zulip chat like Lean! Mathematician beginners — go there and ask some questions about how to do basic maths in Isabelle! Furthermore, Manual Eberl has sent me what he claims is a formalisation of sheaves in Isabelle. But he does not profess to know anything about sheaves — mathematicians who want to learn about sheaves could try using it! Ask him about it in the chat! Let’s get some 21st century mathematics formalised in Isabelle/HOL! ]
Mathematicians
Finally — mathematicians. Is it not easy to believe that at some point in the future, one or more of these systems will be helping us to do mathematics? Are you interested in making this happen sooner? Then why not get involved? In your spare time, learn how to use one of these systems. If you have time, learn how to use all of them and then figure out which one has the most potential. How to learn a system? Think of a maths question that you want to state or prove (could be anything from solving a simple logic problem to stating the Poincare conjecture), and then start asking how to do it. If you want to try Lean then you can ask on the Lean Zulip chat (login required, real names preferred, be nice). Here you find a community of mathematicians and computer scientists who are working out how to communicate with each other, and are isolating specific problems in the way of getting fashionable mathematics into Lean, and then solving them. Somebody there will be able to answer your question. We know exactly what Lean 3 can do in theory and has done in practice, we know where the problems are and we are hoping that they are fixed in Lean 4. But it doesn’t have to be Lean. Try any system! Get involved! It’s fun! It turns theorem proving into solving levels of a computer game. There are some areas of basic mathematics where you have enough control to make this quite a fun computer game, and as time goes on more API will appear, and levels in more and more areas of mathematics will become available. Computer scientists are really interested in how we solve these levels, because they need data. Sarah Loos from Google AI explicitly raised this issue with me at AITP last year. She was bemoaning the fact that in a typical database, a theorem will have exactly one proof. Everyone knows that different proofs can add different value to a situation, by giving different insights. She wants more proofs! These people need our input! But we can’t use the systems so it’s hard for us to give it to them. Learn a system! Prove a theorem! Write a function!
Xena 
> What if an undergraduate wants to try formalising the Hilbert basis theorem?
Hilbert’s basis theorem is the same as Dickson’s lemma and a constructive proof of the result can trivially be obtained from the constructive Coq proof of Ramsey’s theorem to be found in Coquand et al “Stop when you are almost full” (ITP 2012).
LikeLike
But where is the documentation which makes it easy for a random undergraduate mathematician to do this without being guided by an expert? Where is *the way in*?
LikeLike
Lean’s documentation is pretty severely deficient as well, when you want to find the way into using some part of mathlib. Most of the mathlib documentation is just a list of APIs, which does not make for a good manual (this is an extremely common deficiency in documentation for software libraries in general, not limited to Lean). That list is arranged entirely by how the mathlib source code is arranged, which doesn’t help if I’m looking for the name of some trivial result about integers and the result I want is actually proved for something more general like totally ordered monoids (I shouldn’t have to work out what the most general algebraic structure something is true for is in order to find what it’s called). Does the Lean core library have documentation even at the level of a list of APIs? Why are the basic interfaces for things like natural numbers, integers, and various algebraic structures they are instances of, split between the core library and mathlib, so giving two places to look for anything, anyway? Why do parts of the core library seem to use different conventions from mathlib? Where is the documentation of things that can’t readily be deduced from an API list, such as how to choose between multiple similar but slightly different interfaces that look the same to a mathematician but where one might end up more convenient than another for a formal proof?
The natural number game provides a way into proving things with tactics. But as soon as you want to prove something that isn’t just that sort of trivial result about natural numbers, you need a way into the API, and an enormous list of interfaces, with no higher-level guidance on which interfaces to choose and how best to use them, and excluding many of the more basic interfaces because they’re in Lean’s core library rather than mathlib, is not a good way in.
LikeLiked by 2 people
Joseph I finally got around to looking at your BMO2 Lean solutions this weekend and I am extremely impressed about how much Lean you have picked up just by “self-study”. Of course everything you say in your post is correct, and in particular we could certainly do with more infrastructure. Regarding naming of lemmas — there is a convention which we try to stick to (the documentation is here), and the `library_search` tactic will search the library for a lemma you need. A combination of knowing the convention and using ctrl-space in VS Code gets me a long way.
The Lean/mathlib split (random bits of maths are in core, then supporting libraries are in mathlib) is historical and will change in Lean 4. The issue of how to choose between multiple similar but slightly different interfaces (for example there are several ways to deal with the finiteness of a set or type) is complex and in practice the best way to know how to proceed is to ask on the chat. Whatever the deficiencies of our system are, the chat is an extremely powerful way of getting correct answers to all sorts of questions from the mundane to the technical, very quickly.
LikeLiked by 1 person
Here’s one way an undergraduate could find a way in to work on the basis theorem as per above (“Almost Full” development works on Coq 8.11): https://github.com/coq-community/manifesto/issues/97
LikeLiked by 2 people
I know that this is not the answer you might expect but let me ask you anyway: can you become an undergraduate mathematician without being guided by an expert, ie a teacher?
Now I speak only for Coq but I think the point of using a proof assistant and a constructive logic is not only to gain more trust in your proof arguments but to incite you think *differently.* In particular, having to explain the proof to a computer in a *tractable way* invites you to consider several approaches for some definitions which even though equivalent, might impact proof design a lot.
For Coq, this often means thinking inductively. To give an example, as an undergraduate, you basically only know the induction principles for natural numbers: proof by induction and recursive definition of sequences. And when more is needed, the teacher will convert more complex induction to induction on a measure over natural numbers. If not possible, the argument would be based on minimality (which is not the same as induction when the predicate is not decidable). If you follow a set theory course, you will learn induction over an ordinal, ie transfinite induction. But for most undergraduate mathematicians, that is all they know about induction. In Coq, induction is just everywhere, even rewriting using an identity is exactly applying an induction principle. Writing good or tailored induction principles is critical for modular proof designs in Coq.
So of course I do not advocate that the learning curve should be inaccessible for the average undergraduate. However, I think it would be a mistake to try to provide tools that just help the mathematician mimic what he does on paper. A bit like the WYSIWIG vs LaTeX. Is it not better to force yourself learn LaTeX to typeset mathematics than to stick with the cheap approach that does not make you progress?
LikeLike
> Can you really show me that it does not matter that all number fields are countably infinite, and hence biject with each other, and hence are equal, in your system?
I think the premise is false. The carrier sets are equal, but the number fields aren’t.
LikeLiked by 2 people
Pingback: Where is the fashionable mathematics? – Hacker News Robot
I definitely agree with the main point you are making: popular mathematics can and _should_ be done in these proof assistants. I feel, however, that it is not as straightforward as you make it sound and there are deeper issues than the entry barriers. Doing mathematics in type theory usually requires a change in perspective towards the mathematical theory itself: it needs to be understood (1) constructively and (2) predicatively.
I think the perfect example is topology. We start out with the simple question of carrying out topology in type theory. Fundamental theorems of topology such as Tychonoff require classical reasoning so is it even worth doing if we will not be able to computationally prove those in type theory? My personal opinion would be no. Of course, some people like postulating classical axioms and that is fine if one is not interested in a computational understanding of the results, but more serious is the impredicativity involved in topology as explained in the very beginning of [1].
One way of understanding topology constructively is _pointless topology_ [2], which is different from topology that is taught to undergraduates. In fact many “working” topologists don’t know or don’t care about it, really. Here is a quote by Johnstone [2, pg. 46] that explains it well:
> It is here that the real point of pointless topology begins to emerge; the difference
between locales and spaces is one that we can (usually) afford to ignore if we are
working in a “classical” universe with the axiom of choice available, but when (or if)
we work in a context where choice principles are not allowed, then we have to take
account of the difference—and usually it is locales, not spaces, which provide the right
context in which to do topology. This is the point which, as I mentioned earlier,
André Joyal began to hammer home in the early 1970s; I can well remember how, at
the time, his insistence that locales were the real stuff of topology, and spaces were
merely figments of the classical mathematician’s imagination, seemed (to me, and I
suspect to others) like unmotivated fanaticism. I have learned better since then.
I suspect this is the reason why proof assistant people do not have much interest in popular mathematics, because of the feeling that they are the “classical mathematician’s imagination” and it is not even clear what they mean in type-theoretic terms (by which I mean constructively and predicatively).
To understand topology predicatively, we need to further refine pointless topology by focusing on _formal_ presentations of pointless topologies; this is the approach of formal topology, pioneered by Martin-Löf and Sambin [3].
Coq has an impredicative universe and it also allows us to postulate classical axioms so we should not have to bother with any of this stuff, right? I feel that this is the problematic stance here; this is not the correct use of type theory and it just feels wrong when one does this.
Johstone makes a really good point in the quote I included; one can not only study the “real stuff of topology” through pointless topology but can understand it even more clearly. So why do we feel obliged to formalise traditional point-set topology as is? Why not just distil the moral of the story? I think that the only way to achieve the goal of accessible popular mathematics in proof assistants is to embrace that there is a theoretical effort involved, which is not entirely unjustified, and to abandon the obsession with “sets of points” right from the start. It is not a coincidence that the proof assistants you listed are implementations of type theory rather than set theory: if we will write something down as a program, we would like it to be as close as it can be to a program meaning it should be constructive and predicative. Therefore, I find it natural when people use tools that present radical novelties for the way mathematics is done, but have no interest whatsoever in how these tools can simplify and improve our understanding of the mathematical theory of interest.
[1]: Coquand, T. et al. 2003. Inductively generated formal topologies. Annals of Pure and Applied Logic. 124, 1–3 (2003), 71–106. DOI: https://doi.org/10.1016/S0168-0072(03)00052-6.
[2]: Johnstone, P.T. 1983. The point of pointless topology. Bulletin of the American Mathematical Society. 8, 1 (1983), 41–53. DOI:https://doi.org/10.1090/S0273-0979-1983-15080-2.
[3]: Sambin, G. 1987. Intuitionistic Formal Spaces — A First Communication. Mathematical Logic and Its Applications. D.G. Skordev, ed. Springer US. 187–204.
LikeLiked by 1 person
Unfortunately I *absolutely reject* your assertion that mathematics needs to be understood constructively in order to make progress. In fact I believe the exact opposite — that the continual assertions from parts of the CS community that constructivism is of utmost importance builds a *huge* barrier to formalising “fashionable mathematics” in theorem provers. In my work with Massot and Commelin formalising the definition of a perfectoid space there are many many times when we work classically, and in our forthcoming work where we will construct examples of perfectoid spaces it is just the same. Constructivism might be popular in computer science circles, but in maths departments it is completely ignored. LEM is used absolutely essentially, all over the place, in the work of the four recent Fields Medallists, *even in the statements of their results* (this is slightly counterintuitive, but even to define some of the objects which are being talked about one has to prove theorems and these theorems are not true constuctively).
I am well aware of constructivism and the work which is going on in this area. However, within mathematics departments, the prevailing view is that Hilbert won the argument 100 years ago and we have not looked back since, despite what constructivists want us to believe. Constructive mathematics is a *NON-STARTER* in 99% of mathematics done in mathematics departments, and what I would like to focus on is getting mathematicians to use theorem provers so LEM and AC (or at least countable dependent choice, which we all *need*) absolutely have to be on the table. If you don’t want to give me them in your system, that’s fine — but I won’t be using your system and I can absolutely assure you that my colleagues will feel the same way. The debate has moved on in mathematics departments. Lean offers me exactly what I need — LEM, full AC, noncomputability, and still the ability to reason.
LikeLiked by 2 people
> If you don’t want to give me them in your system, that’s fine — but I won’t be using your system and I can absolutely assure you that my colleagues will feel the same way. The debate has moved on in mathematics departments.
I completely understand this. The concern I was trying to express was: if the goal is to get more mathematicians to use formal reasoning tools, why not choose tools that implement exactly their native language? Type theory was built as a clarification of the language of constructive mathematics and it will naturally seem foreign to people whose job is to develop classical mathematics. In short, would you prefer Lean over a set-theoretic reasoning tool of equal quality? If so, what do you think makes type-theoretic tools advantageous for people who want to formalise set-theoretical developments in it?
When a classical mathematician starts studying a system like Coq, he has to first learn about type-theoretical mathematics as well as the technical intricacies of using such a formal system. The latter is inevitable but it seems to me that the difficulty caused by the former could be avoided by using set-theoretical tools.
LikeLike
My take on it is that formalising in set theory is like writing computer programs in machine code, and formalising in type theory is like writing programs in a more high-level language. In particular type theory gives me an easy way of manipulating high-level mathematical objects like topological spaces or schemes without having to worry that they are in fact ordered quintuples of sets or whatever. It might be true historically that type theory was strongly linked to constructive mathematics, but Lean’s type theory + LEM + AC + noncomputability works fine for me doing classical mathematics, and in fact is the main reason that I am devoting time into leaning Lean rather than Coq or the HoTT systems.
LikeLike
You are talking about what happens now in math departments, but this is not a proof that this paradigm will be correct forever. Your view of constructivism is blocked to 100 years ago, and marred with ideological prejudices. My suggestion is, if you are young enough, to open up your mind a bit.
Giovanni Sambin
LikeLike
You are absolutely right that I am prejudiced against constructivism, because my target audience is people interested in the kind of geometry, topology, number theory etc which is going on in most mathematics departments across the world, and here, rightly or wrongly, constructivism is not at all well represented — in fact I would go so far as to say that most geometers, topologists, number theorists etc do not really know what constructivism is. I am trying to change the way that these “generic mathematicians” feel about theorem provers — these people are my target audience — so I personally stay well away from constructivism. People like Thorsten Altenkirch have said to me that it is a very sad state of affairs that constructivism has basically been rejected in most mathematics departments and has argued coherently to me that there should be a place for it. But constructivism is not taught in a typical undergraduate degree, except perhaps in one optional course on logic, lost amongst the sea of courses on manifolds, Banach spaces, differential equations, elliptic curves, topology etc, all of which heavily rely on classical logic and the axiom of choice. If I were to be fighting against this and telling geometers etc to work constructively, people would say I was crazy, and all the literature would need to be rewritten. It’s not going to happen. Showing mathematicians how to do formalised mathematics in classical logic using the axiom of choice is the path which I have determined has the best chance of success. I agree that I have no idea what will be happening in 100 years’ time, but the theorems which the Fields Medallists are proving are simply not true constructively, and I find it hard to envisage a future where mathematical society decides to reject these results.
LikeLike
My reply:
https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ
LikeLike
Xenaproject
“You are absolutely right that I am prejudiced against constructivism.”
I fully appreciate your frank answer. Being aware of your prejudices is perhaps the most important step to overcoming them. As you know, most mathematicians are not aware of them. So that’s very good. I like very much to start a discussion in this way, when ideological choices are set down so clearly and openly. I will be equally frank in my answers. My ideology is rather different. I happened to land at this webpage only because I was looking for recent mentions of formal topology. Now that I read a bit more about your project and your opinions, I will be just a bit more cautious than in my first comment. I apologise for my approximate English.
Personal choices are in the end a matter of cultural and political visions. In my view, it’s like the choice between agriculture with chemical fertilisers or with biodynamics only. At the moment, the former gives far greater agricultural yield, but as many are beginning to see it kills bees and in general it destroys the environment. Constructive mathematics is respectful of our mental environment. My long term aim is to show that you do not loose anything by following it. Actually, the contrary.
Another metaphor is with economy; the fact that capitalism is the most common does not change its destruction of the environment, either directly or indirectly (e.g. through social injustice).
You seem to accept the common trend and follow it. I am crazy enough that I try to change it and to engage my life to achieve that.
I hasten to add that it is not (only) a matter of ideology. There are lots of technical advantages in constructive mathematics (in particular my brand): no waste of information, much simpler proof-search, modular, compatible with other approaches, reliable.
If I had to undergo a delicate computer-assisted surgery or I had to take a plane Boeing 737, I would be very willing to pay much more if I know that the underlying proof-assistant is based on UF rather than ZFC (that has no cut-elimination procedure, i.e. no proof of termination), and even more if it is based on our Minimalist Foundation MF.
Contrary to common cliches, constructive mathematics is a very powerful and sophisticated tool. It is like using a scalpel rather than a butcher’s knife for surgery. When mathematicians will grasp this, rather than seeing it as an amputation of classical mathematics, perhaps things will change.
Xenaproject:
“There is a large community of mathematicians out there who simply cannot join these communities because the learning curve is too high and much of the documentation is written for computer scientists.”
Constructive mathematics, in particular if done in my “minimalist” style, is much closer to proof-assistants than classical mathematics. Much of my new topology has been implemented (in Matita) with de Bruijn factor 1! So my approach could help mathematicians to cover their distance from computer assisted mathematics.
“You might simply decide to reject the idea that formalising fashionable mathematics is important. And this is fine. But, in return, don’t expect us to come and join your community. You might not want us! This is fine! But we represent true potential for growth.”
I agree. But then this should be reciprocal. Again, you seem to put it in terms of “us against them” which is very ideological, and closed to real exchange. “We” constructivists know well what the classical approach is, and precisely because of this we are interested in improving it. It is not a rejection based on prejudice. I wrote a few papers whose content works only classically; they are still cited after 30 years.
“univalent people […] really do not seem to care about doing “fashionable mathematics”. ”
Funny, since Vladimir Voevodsky started all this business from very fashionable mathematics, enough to win a Field medal.
“Assia Mahboubi is someone who is actually doing mathematics in Coq which “proper mathematicians” are interested in. She cannot do it alone! ”
Why don’t you join her?
Dominique Larchey-Wendling
“For Coq, this often means thinking inductively.”
Thierry Coquand and I (mainly) have introduced inductive methods in topology. This was totally unexpected from the perspective with points. This means a lot of effectivity, that proof-assistants are excellent in exploiting, that classically had been completely ignored.
Later Thierry, Lombardi and others have shown also how powerful these methods are in abstract algebra.
” Is it not better to force yourself learn LaTeX to typeset mathematics than to stick with the cheap approach that does not make you progress?”
Excellent point, I fully agree. I learned Latex, btw, in mid 80s.
Ayberk Tosun
“Doing mathematics in type theory usually requires a change in perspective towards the mathematical theory itself: it needs to be understood (1) constructively and (2) predicatively.”
That is exactly my own experience of over 30 years. I can only add that working in the actual development of topology over a predicative and intuitionistic foundation has delivered some other novelties, beyond inductive methods. I am trying to finish writing a book on this, together with an exposition of my own “philosophy” (which I’m doing right now and is the most difficult part). One of the insights is that motivations for the pointfree approach to topology are even more pressing than those described by Johnston. Briefly, to maximise effectivity and hence improve efficiency of implementation in a proof-assistant.
“I think that the only way to achieve the goal of accessible popular mathematics in proof assistants is to embrace that there is a theoretical effort involved, which is not entirely unjustified, and to abandon the obsession with “sets of points” right from the start.”
I agree, although I also believe this abandoning will not be painless (or painfree).
Xenaproject
“LEM is used absolutely essentially, *even in the statements of their results* ”
I agree, and that is one of the big problems. Assuming that LEM is just “the truth” for example mathematicians define closed = complement of open, which is equivalent to closed = contains its limit points only classically (more precisely, the equivalence of the two definitions is equivalent to LEM). Thus for over 60 years they did not see a logical duality between open and closed, much deeper than complement. It was me to find it in the 90s only because I was not assuming classical definitions for granted.
“the prevailing view is that Hilbert won the argument 100 years ago ”
I agree, but unfortunately this was not by intellectual superiority, rather by brute force (a sort of McCarthyism in mathematics, see below), and we still pay the negative consequences (as your prejudice towards constructivism shows well).
“so I personally stay well away from constructivism.”
Just as many people stayed well away from whatever smelled communism during McCarthyism in US in the 50s! You are just depicting a typical example of rejection on ideological grounds, not knowledge. So one of the inventors of general topology in the modern sense, John Kelley, lost his position in Berkeley based on suspicions (he was just truly democratic). What a nice, open and inspiring society to live in!
“If I were to be fighting against this [rejection of constructivism] and telling geometers etc to work constructively, people would say I was crazy.”
I am sorry to tell you that you are now discussing with one of these crazy guys, even more radical than Thorsten (even if we agree on a lot of matters) . Refusing to work constructively, geometers have been unable to see how to embed topological spaces into Grothendieck toposes, something that I am able to do (after a suitable improvement of Top). I am ready to discuss if my way is really a solution or just a trick. But it remains a fact that in over 60 years nobody found it in the classical environment.
“the theorems which the Fields Medallists are proving are simply not true constructively, and I find it hard to envisage a future where mathematical society decides to reject these results.”
It is not necessary to reject them, they will never become “false” but rather less interesting. The opinion that mathematical truth is given and unique is a typical hoax set up to support the dominant ideology (as it happens with economy). Mathematics is dynamic and hence plural.
It was very good for me to spend some time in this dialogue with you. I hope the same will apply to you. For me, it gave new motivation to go on and finish the book on constructive topology I am writing.
Giovanni
LikeLike
My decisions to formalise classical mathematics in Lean are nothing to do with any “philosophy” of my own. I just view classical mathematics as a game, and constructive mathematics as a different game. What I want to do is to make the “dominant mathematicians” (I like this phrase!) notice proof assistants, because I work with proof assistants and I want funding, and the dominant mathematicians are in charge of funding. And to do that I feel like I have to appeal to them in the language they are using, and that language is classical.
People have checked very carefully that e.g. Deligne’s proof of the Weil conjectures, or the Wiles/Taylor proof of FLT, fit into ZFC set theory. But more recently people have started using infinity categories and I wonder whether in 20 years’ time there will be a new discussion, between people who want to stick to ZFC and people who want to use universes in either a serious way, or a possibly non-serious way but they never check it’s non-serious and nobody who understands the material is interested in foundations enough to check.
LikeLike
I see your position, but I confess I am unable to share it, even the little bit that could be sufficient to continue our discussion. I have dedicated my life to mathematics, and I am unable to do that while believing it is a game of which I don’t understand the meaning. We clearly have deeply different motivations. I am glad we got to know each other. Good luck.
LikeLike
As Xena’s Twitter account already published (https://twitter.com/xenaproject/status/1380935053409198080), Sheaves have been now formalized in Isabelle/HOL (https://www.isa-afp.org/entries/Grothendieck_Schemes.html). Maybe you can update your post accordingly and hint at the role locales play in making Isabelle’s type system much richer than it seems.
LikeLike
Yes, I was very happy to see this work! It’s on my job list for this week to take a closer look at the paper, coincidentally. Perhaps I will say more about this when I’ve read it.
LikeLike
OK I finally looked seriously at the paper (I am scared of formalisation papers in languages other than Lean 🙂 ). So it is absolutely brilliant that they defined schemes in Isabelle! I am a bit scared though that they seemed to have to make a completely new definition of ring though, which means that they will not be able to use any of the existing API for commutative rings in order to develop the theory any further.
LikeLike