https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...
[1]: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...
"Proof assistants can’t read a maths textbook, they need continuous input from humans, and they can’t decide whether a mathematical statement is interesting or profound — only whether it is correct, Buzzard says. Still, computers might soon be able to point out consequences of the known facts that mathematicians had failed to notice, he adds."
This is an issue, but there's an established practice of writing formal sketches where the gaps in the proof are explicitly marked, and future tooling might bring ways to address these gaps once a full formal context is provided.
One issue is that Lean has little or no support for declarative proof, which is by far the most natural setting for these "proof sketches", and also brings other advantages wrt. complex proofs. (Coq has the same issue; some code was written to support declarative proofs, but it was too buggy and bitrotted, so it got removed.)
At least give a proper reference to what you're alluding to, please.
Also, closeness in AI has shown to be a misleading concept.
This is about some pretty creative uses of computing in maths and bugger all to do with AI (whatever that is.)
If you put enough blood, sweat and tears into codifying mathematical concepts into Lean, you can feed it a mathematical thingie and it can tell you if that thingie is correct within its domain of knowledge. If you get an "out of cheese error", you need to feed it more knowledge or give up and take up tiddlywinks.
This explains Lean in terms I can understand: https://www.quantamagazine.org/building-the-mathematical-lib...
I recall that the Fermat's proof linked several normally disparate areas to get to the meat of the issue.
Simply tagging those relations to identified sub-fields of study will probably help give guidance to impacts of theories, maybe farm them out to advanced students for quick review.
I spent some time previously playing with Coq. It's very powerful, but even proving the simplest undergraduate maths statements (say, about group theory) can prove very challenging. I believe that part of this is that Coq uses different mathematical foundations than traditional mathematics, which mostly uses set theory (ZFC, although most people don't care about the specifics). So it can be hard or unnatural to express something like "subgroup". I don't know if Lean fares better in that respect. Coq documentation is also IMHO almost impossible to understand unless you're already very deeply knowledgeable about the system.
We will probably still need some more iterations, to get more user friendly assistants with better documentation and to get adequate teaching resources etc.
The issue is rather that you need to deal with edge cases that are usually swept under the rug, or that you need to spend a full page working out the details of a proof that everyone recognizes as obvious. It would be great if computers could give even more assistance with these tedious parts of formalization, and I'm very glad that people are working hard on realizing this.
(Thanks to Curry-Howard, we can also view this as generating test suites/specifications for software libraries!)
Notable tools include Hipster, IsaScheme, IsaCoSy, QuickSpec and Speculate.
Given a group G, there is a type `subgroup G` of subgroups of G, and a subgroup is a structure consisting of a set of elements of G along with some proofs that it has the identity, it's closed under multiplication, and it's closed under taking inverses. Lean has a coercion facility using typeclasses, and there is a typeclass instance that will use the subgroup's set coerced to a type when the subgroup is used in a place that expects a type. This coerced type has a group typeclass instance, so a subgroup "is" a group.
The big complexity in all of this doesn't seem to be ZFC vs type theory, but rather how do you implement a mathematician's use of synecdoche and implicit coercions. Synecdoche is the figure of speech where you refer to a thing by its parts or vice versa -- for example, "let G be a group" and then using G as if it were a set, even though a group consists of a set, a binary operation on the set, a choice of identity element, and a few axioms that must hold. Mathlib uses typeclasses to implement the synecdoche -- a type is a group if there is a typeclass instance that provides the rest of the structure. As I understand it, Coq's Mathematical Components library uses structures and unification hints instead (though I've failed to understand how it works exactly), but I have heard that they can be very fiddly to get right.
I think you'd have to find solutions to these same problems no matter the foundations. At least with types, there's enough information lying around that, for example, group structures can be automatically synthesized by the typeclass resolution system in many common situations.
Most activity in proof systems is based in type theory these days, but set theoretical systems do exist, of which Metamath is the most mature. That said, Metamath is seriously lacking in automation, so there is an element of tedium involved. That's not because of any fundamental limitations, but I think mostly because people working in the space are more motivated to do things aligned with programming language theory. There was also a talk by John Harrison a few years ago proposing a fusion of HOL and set theory, but I'm not sure there's been much motion since then.
I believe a fully featured proof assistant based in set theory would be a great contribution.
[1] https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html
“ The crucial point of condensed mathematics, according to Scholze and Clausen, is to redefine the concept of topology, one of the cornerstones of modern maths. A lot of the objects that mathematicians study have a topology — a type of structure that determines which of the object’s parts are close together and which aren’t. Topology provides a notion of shape, but one that is more malleable than those of familiar, school-level geometry: in topology, any transformation that does not tear an object apart is admissible. For example, any triangle is topologically equivalent to any other triangle — or even to a circle — but not to a straight line.
Topology plays a crucial part not only in geometry, but also in functional analysis, the study of functions. Functions typically ‘live’ in spaces with an infinite number of dimensions (such as wavefunctions, which are foundational to quantum mechanics). It is also important for number systems called p-adic numbers, which have an exotic, ‘fractal’ topology.”
"For example, any triangle is topologically equivalent to any other triangle — or even to a circle — but not to a straight line."
Is it because triangles and circles are "2D" and lines aren't?
But you can't get a straight line - to do that you need scissors to cut one point of a circle (to be precise, remove a single point) - and then you can stretch the remainder to infinity and now you have your line.
You can give this function explicitly. Let's assume that the triangle is drawn on a piece of paper with an x and y axis, such that the intersection of the axes (the origin) is inside the triangle. For each point on the triangle, draw a line from the origin to the point. Take the angle between that line and the x-axis. Use that angle to map it onto a circle.
It's because triangles are loops (closed) and straight lines aren't.
Essentially our civilization progressed to the point where computers started to take more of a role in new discoveries much like in the real world. As computers got more powerfull and AI developed naturally scientific advancement sped up. But there came a point when the science and math became too advanced for humans to even comprehend, so computers did it. Then there came a point when things were so advanced that even scientists couldn't even ask the right questions so an AI intermediate would have to be used.
Then things get weird and you have the 40k universe.
Anyways I know I probably butchered it a little but that's the gist of it and I can totally see things progressing in the real world up to the point where things get weird in 40k.
I don't mind proof assistants as a way to gain new insights into mathematics, but I worry that maths is drifting into a direction where it turns more into hermeneutics than actual mathematics. The automation of proofs isn't the only thing, I also was very scpetical about the whole process of Shinichi Mochizuki's proof of the abc conjecture.
The whole circus around Mochizuki's proof of the abc conjecture was dealt with quite well by the social structure of the mathematical community. Many people looked at the proof. Many people got stuck. Several experts got stuck at exactly the same point. And Mochizuki refuses to acknowledge that there is a problem at that point of his "proof". But a consensus was reached in the mathematical community (maybe minus RIMS).
https://en.wikipedia.org/wiki/The_Man_Who_Loved_Only_Numbers
Mochizuki's stuff is simply a hypercomplicated pile of nonsense unintelligible to the mathematical community.
I would add current automated proof systems. IMHO we are just at the beginning that mathematicians realize the usefulness of technology, which was basically neglected ever since.
Related to the unexplainability of AI. We're just grasping for more than we can hold in our little working memory.
As far as I can see this is just programming. How is this different from writing in Java
int i = “hello”
Of course, we need more complex types than “int” and “String”, but in principle it’s the same.
However, the cool thing about programming is that it lets us represent a lot of different things. In this case you're representing the construction and interaction of mathematical objects, with a language that targets a specific proof management system to verify this constructions.
But yes, it is "just programming", and some functional languages even support proofs to some extent like Scala or Agda.
> Or does it "contain" topology in some sense, allowing people to continue working with notions of convergence obtained from norms?
has a positive answer. You can, if you want, swap out topological spaces, and use condensed sets instead, and just continue with life as usual.
At the same time, all of this is in fast paced development, so hopefully we will see some killer apps in the near future. But I expect them more in the direction of Hodge theory and complex analytic geometry.
You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever found a proof of `false` so far in Lean 3.
The choice for Lean is actually quite natural: (i) it has a large and coherent library of mathematics to build such a project upon. And (ii), it has a substantial user base of mathematicians somewhat familiar with the subject at hand (i.e., condensed mathematics).
The initial challenge by Peter Scholze was directed at all theorem proving communities. As far as I know, only the Lean community took up the challenge.
(Concerning Lean 4: yes, mathlib will have to be ported. And yes, people are working hard on this. I think that none of the theorem provers so far are ready for wide-scale use in mathematics. And that's why it is important to iterate fast. The Lean community is not afraid of redesigns and large refactors when discovering better approaches.)
You are right, my bad. Taking my words back on that.
A bit more details from the Pierre-Marie Pédrot:
> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around.
> The first thing they do is to axiomatize quotient types, which is somewhat fine and can be done the same in Coq. As any use of axioms, this breaks canonicity, meaning your computations may get stuck on some opaque term. (While slightly cumbersome, axiomatizing quotients already solves 99,9% of the problems of the working mathematician).
> Now, were they do evil things that would make decent type theorists shake in terror, they add a definitional reduction rule over the quotient induction principle. We could do the same in the Coq kernel, but there is a very good reason not to do this. Namely, this definitional rule breaks subject reduction, which is a property deemed more important than loss of canonicity.
> In Lean, you can write a term t : A where t reduces to u, but u doesn't have type A (or equivalently may not typecheck at all). This is BAD for a flurry of reasons, mark my words. Reinstating it while keeping quotients requires an undecidable type checking algorithm, which is another can of worms you don't want to wander into. The same kind of trouble arises from similar Lean extensions like choice.
About incompatibility: Last time I checked (some 3 or so years ago), Coq was not backwards compatible either, and libraries had to be ported manually with each update. Sadly, as this is the one greatest anti-feature that is currently putting me off proof assistants, but probably it needs some time, and the quickest way to get there is to maximize usage. From what I know about Coq and Lean, I suspect Lean will stabilize faster than Coq does, due to it being more "declarative" (Coq is based too much on complex tactics, which are hard to make stable by design).
With verifiers like this as a useful tool, I'm guessing in the coming years this LoC will be dwarfed.
I'm a bit surprised a theorem of major complexity reduced to that small a LoC count.
This has me in awe about the depth of mathematics, the pace of progress, the miracle of specialisation. I have a degree in an applied-math-y adjacent field, and understand nothing. (And, btw, I was astonished how knowledgable some commenters right here were, and then realised that we have the (co-)authors of the results themselves here! gotta love HN.)
With that said, here some (non-mathematical) snippets I found interesting (apart from the great word "sheafification"):
> Why do I want a formalization?
> — I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. In the end, we were able to get an argument pinned down on paper, but I think nobody else has dared to look at the details of this, and so I still have some small lingering doubts.
> — while I was very happy to see many study groups on condensed mathematics throughout the world, to my knowledge all of them have stopped short of this proof. (Yes, this proof is not much fun…)
> — I have occasionally been able to be very persuasive even with wrong arguments. (Fun fact: In the selection exams for the international math olympiad, twice I got full points for a wrong solution. Later, I once had a full proof of the weight-monodromy conjecture that passed the judgment of some top mathematicians, but then it turned out to contain a fatal mistake.)
> — I think this may be my most important theorem to date. (It does not really have any applications so far, but I’m sure this will change.) Better be sure it’s correct…
> In the end, one formulates Theorem 9.5 which can be proved by induction; it is a statement of the form ∀∃∀∃∀∃ (\forall \exists \forall \exists \forall \exists), and there’s no messing around with the order of the quantifiers. It may well be the most logically involved statement I have ever proved.
> Peter Scholze, 5th December 2020 [2]
Question: What did you learn about the process of formalization?
Answer: I learnt that it can now be possible to take a research paper and just start to explain lemma after lemma to a proof assistant, until you’ve formalized it all! I think this is a landmark achievement.
Question: And about the details of it?
Answer: You know this old joke where a professor gets asked whether some step really is obvious, and then he sits down for half an hour, after which he says “Yes, it is obvious”. It turns out that computers can be like that, too! Sometimes the computer asks you to prove that A=B, and the argument is “That’s obvious — it’s true by definition of A and B.” And then the computer works for quite some time until it confirms. I found that really surprising.
Question: Was the proof in [Analytic][4] found to be correct?
Answer: Yes, up to some usual slight imprecisions.
Question: Were any of these imprecisions severe enough to get you worried about the veracity of the argument?
Answer: One day I was sweating a little bit. Basically, the proof uses a variant of “exactness of complexes” that is on the one hand more precise as it involves a quantitative control of norms of elements, and on the other hand weaker as it is only some kind of pro-exactness of a pro-complex. It was implicitly used that this variant notion behaves sufficiently well, and in particular that many well-known results about exact complexes adapt to this context. There was one subtlety related to quotient norms — that the infimum need not be a minimum (this would likely have been overlooked in an informal verification) — that was causing some unexpected headaches. But the issues were quickly resolved, and required only very minor changes to the argument. Still, this was precisely the kind of oversight I was worried about when I asked for the formal verification.
Question: Were there any other issues?
Answer: There was another issue with the third hypothesis in Lemma 9.6 (and some imprecision around Proposition 8.17); it could quickly be corrected, but again was the kind of thing I was worried about. The proof walks a fine line, so if some argument needs constants that are quite a bit different from what I claimed, it might have collapsed.
Question: Interesting! What else did you learn?
Answer: What actually makes the proof work! When I wrote the blog post half a year ago, I did not understand why the argument worked, and why we had to move from the reals to a certain ring of arithmetic Laurent series. [...]
Question: So, besides the authors of course, who understands the proof now?
Answer: I guess the computer does, as does Johan Commelin. [Note: = deadbeef57 here on HN][3]
[1] https://mathoverflow.net/questions/386796/nonconvexity-and-d...
[2] https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...
[3] https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...
It's a game implemented in lean, where you work your way through the basic facts about natural numbers.
Especially the "Natural Number Game" under "Learning resources" has been successful in teaching folks the very basics for writing proofs. Once finished, a textbook like "Theorem Proving in Lean" can teach the full basics. Feel free to join the Lean Zulip at any point and ask questions at https://leanprover.zulipchat.com/ in the #new members stream.
Mathlib has plenty of contributions from interested undergrads :)
*I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supplied by the user.
A computer assisted proof is just as correct or helpful, it just may be more complicated of a proof initially. Given time said proof can be simplified but having the proof in the first place allows you to move away from assumptions into proofs or alternatively even open new doors that weren't known to exist.
Keep in mind that these computer aided proofs are equivalent to pen and paper proofs but because you can rely on software to guarantee you haven't made any mistakes, you can make more complex proofs that still work.
It's the same as with programming. You can write overly complex and opaque proofs in the same way you can write bad, slow, or hard to read code. It still "works" but it's not ideal and is often a first revision in a series of steps towards the clean, fast, and easy to read final products.