Zulip Chat Archive
Stream: maths
Topic: ALEXANDRIA: Proof for the Working Mathematician
Sean Leather (May 15 2018 at 12:06):
ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician
L. C. Paulson, Computer Laboratory, University of Cambridge
Mathematical proofs have always been prone to error. Today, proofs can be hundreds of pages long and combine results from many specialisms, making them almost impossible to check. One solution is to deploy modern verification technology. Interactive theorem provers have demonstrated their potential as vehicles for formalising mathematics through achievements such as the verification of the Kepler Conjecture. Proofs done using such tools reach a high standard of correctness.
However, existing theorem provers are unsuitable for mathematics. Their formal proofs are unreadable. They struggle to do simple tasks, such as evaluating limits. They lack much basic mathematics, and the material they do have is difficult to locate and apply.
ALEXANDRIA will create a proof development environment attractive to working mathematicians, utilising the best technology available across computer science. Its focus will be the management and use of large-scale mathematical knowledge, both theorems and algorithms. The project will employ mathematicians to investigate the formalisation of mathematics in practice. Our already substantial formalised libraries will serve as the starting point. They will be extended and annotated to support sophisticated searches. Techniques will be borrowed from machine learning, information retrieval and natural language processing. Algorithms will be treated similarly: ALEXANDRIA will help users find and invoke the proof methods and algorithms appropriate for the task.
ALEXANDRIA will provide (1) comprehensive formal mathematical libraries; (2) search within libraries, and the mining of libraries for proof patterns; (3) automated support for the construction of large formal proofs; (4) sound and practical computer algebra tools.
ALEXANDRIA will be based on legible structured proofs. Formal proofs should be not mere code, but a machine-checkable form of communication between mathematicians.
The project will run for 60 months starting 1 September 2017.
Johan Commelin (May 15 2018 at 12:09):
Wow, those are big claims (-;
Kevin Buzzard (May 15 2018 at 12:18):
Yeah exactly. So I emailed him saying "you're just up the road from me, how come you're not reaching out to mathematicians like me so we can talk about this sort of stuff?" and he said "yeah I'm just sitting in my office like usual really" so I said "OK so you can reach out to me by me coming to visit on Tuesday and you telling me what it's all about" and he said "OK"
Kevin Buzzard (May 15 2018 at 12:18):
I mean, I guess he didn't say _exactly_ that...
Kevin Buzzard (May 15 2018 at 12:19):
but he did remark that someone called Peter Koepke would also be there on Tuesday giving a talk...
Gabriel Ebner (May 15 2018 at 12:20):
At the risk of sounding maybe a bit unimpressed, but I think that this proposal is not overly ambitious. It's basically a continuation of current work in Isabelle. The goals are pretty much 1) formalize some undergrad math, 2) improve the search function a bit, 3) add more refactoring tools, and 4) integrate and polish some computer algebra tactics.
Kevin Buzzard (May 15 2018 at 12:20):
Wow, those are big claims (-;
It's also big money, right? Multi-million pound ERC grant. One of the last the UK will ever get, due to Brexit.
Patrick Massot (May 15 2018 at 12:21):
Such a shame to do this in Isabelle
Patrick Massot (May 15 2018 at 12:21):
He should have come here
Kevin Buzzard (May 15 2018 at 12:21):
Thanks for this Gabriel. In mathematics it seems to be extremely difficult to get these big ERC grants, in the sense that the people I know who have got them recently have put in some very high-powered proposals.
Kevin Buzzard (May 15 2018 at 12:21):
My impression is that he is really into the idea of formal proofs being readable.
Patrick Massot (May 15 2018 at 12:21):
As far as I can see there is no obstruction to having readable proofs in Lean
Kevin Buzzard (May 15 2018 at 12:22):
I mean, human-readable source code
Patrick Massot (May 15 2018 at 12:22):
It's only Mario and Johannes don't like them
Patrick Massot (May 15 2018 at 12:22):
The sledgehammer thing is much more serious issue of course
Kevin Buzzard (May 15 2018 at 12:23):
I sometimes write "low-level" proofs, and I find them very enjoyable (my instincts just tell me to press on instead of trying tactics), but I do feel at the end of it all that they are no more readable than any other Lean code, they are just intro, apply, intro, refine, intro, exact, cases, cases, rwa, done
Kevin Buzzard (May 15 2018 at 12:23):
intros a Ha
Kevin Buzzard (May 15 2018 at 12:24):
Maybe I should be writing intros a proof_that_a_is_in_X
Patrick Massot (May 15 2018 at 12:24):
I often try to do that
Kevin Buzzard (May 15 2018 at 12:26):
Kevin Buzzard (May 15 2018 at 12:26):
"I follow my nose, cases, rw, apply, cases, exact, intro, split, cases, apply, exact"
Kevin Buzzard (May 15 2018 at 12:27):
and voila, Spec(R) is compact
Patrick Massot (May 15 2018 at 12:27):
I don't think it would be hard to make it easier to read
Patrick Massot (May 15 2018 at 12:27):
You already have a couple of explicit have
Kevin Buzzard (May 15 2018 at 12:27):
I agree
Kevin Buzzard (May 15 2018 at 12:28):
it was certainly easy to write :-)
Kevin Buzzard (May 15 2018 at 12:28):
but my point is that I didn't
Kevin Buzzard (May 15 2018 at 12:28):
make it easy to read
Patrick Massot (May 15 2018 at 12:28):
You could add a few more, maybe with some suffices
Patrick Massot (May 15 2018 at 12:31):
Why "quasi-compact" if you prove compactness?
Kevin Buzzard (May 15 2018 at 12:33):
I thought that this was the French's fault?
Kevin Buzzard (May 15 2018 at 12:34):
In the UK, compact := every cover has a finite subcover. In France it's Hausdorff + ...
Kevin Buzzard (May 15 2018 at 12:34):
but alg geom is a French subject
Kevin Buzzard (May 15 2018 at 12:34):
because schemes are typically not Hausdorff, it's quasi-compact
Kevin Buzzard (May 15 2018 at 12:36):
PS @Gabriel Ebner when writing grant proposals, you write what you think will get funded (so you get a promotion or pay rise when you get the grant), and then you just keep on doing what you were doing beforehand anyway (at least that's what happens in maths).
Kevin Buzzard (May 15 2018 at 12:37):
One might also ask why computer scientists have been sitting on things like Coq / Isabelle for decades, and these are perfectly capable of formalising all of undergraduate pure mathematics, but nobody has done it yet.
Patrick Massot (May 15 2018 at 12:41):
Oh, I understand: you mean mathlib's definition of compactness is the broken one (without Haussdorff)?
Kevin Buzzard (May 15 2018 at 12:41):
right
Kevin Buzzard (May 15 2018 at 12:41):
it's only broken because of your cultural upbringing
Kevin Buzzard (May 15 2018 at 12:41):
One could instead regard it as a translation issue
Kevin Buzzard (May 15 2018 at 12:41):
English "compact" := French quasi-compact
Kevin Buzzard (May 15 2018 at 12:42):
Like UK N := France N^0 or N^* or whatever you call the thing without a zero.
Patrick Massot (May 15 2018 at 12:42):
Anyway, I don't understand how proving quasi-compactness can be anything but trivial in algebraic geometry: any open set covers almost everything!
Kevin Buzzard (May 15 2018 at 12:42):
well I did point out that my proof was just 50 lines of intro, apply, exact ;-)
Patrick Massot (May 15 2018 at 12:46):
To be honest I have no idea where this difference comes from. All spaces I work with are obviously Haussdorff, so I never say or write quasi-compact
Johan Commelin (May 15 2018 at 12:54):
But then, you forget saying Haussdorff half the time!
Kevin Buzzard (May 15 2018 at 13:19):
He's using type class inference
Kevin Buzzard (May 23 2018 at 07:26):
Did you get any insights with the ALEXANDRIA / Peter Koepke lecture person today?
yesterday
Kevin Buzzard (May 23 2018 at 07:27):
That was an interesting day
Kevin Buzzard (May 23 2018 at 07:27):
I'll talk about it later, I need to go and do family stuff for 30 minutes
Kevin Buzzard (May 23 2018 at 08:31):
So Koepke gave a nice talk about some system that they got going which checks ZFC proofs and whose parser parses statements which look like natural language
Kevin Buzzard (May 23 2018 at 08:31):
I personally don't know how much importance to attach to the concept that a computer-checked proof should be human-readable
Kevin Buzzard (May 23 2018 at 08:31):
And after that there was a long discussion
Kevin Buzzard (May 23 2018 at 08:32):
for over 2 hours
Kevin Buzzard (May 23 2018 at 08:32):
where we just talked about life and where all this was going
Kevin Buzzard (May 23 2018 at 08:33):
Koepke had taken someone else's Haskell code written in 2008 and got an MSc student to understand it and rewrite it better
Kevin Buzzard (May 23 2018 at 08:33):
Their system is called SAD
Kevin Buzzard (May 23 2018 at 08:33):
and they are producing "miniatures", i.e. relatively short proofs which rely on a lot of assumptions which are axioms
Kevin Buzzard (May 23 2018 at 08:34):
e.g. they proved something about successor cardinals being regular but assuming things like kappa x kappa = kappa etc
Kevin Buzzard (May 23 2018 at 08:34):
what his point was, was that the proof script is genuinely human-readable
Kevin Buzzard (May 23 2018 at 08:34):
and everyone dreamt about having all 1st and 2nd year UG maths in their system
Kevin Buzzard (May 23 2018 at 08:35):
but I think that only I have a coherent strategy for making this happen
Kevin Buzzard (May 23 2018 at 08:35):
i.e. getting 1st and 2nd year UGs to put it into the system themselves
Kevin Buzzard (May 23 2018 at 08:35):
and we all moaned about how the Cauchy Integral Formula was hard
Kevin Buzzard (May 23 2018 at 08:36):
and Paulson even had an anecdote about it
Kevin Buzzard (May 23 2018 at 08:36):
having translated Harrison's proof from (something) into (something)
Kevin Buzzard (May 23 2018 at 08:36):
maybe from HOL light into Isabelle?
Kevin Buzzard (May 23 2018 at 08:37):
and there was some subtlety about whether the curve you were integrating around was differentiable or continuously differentiable
Kevin Buzzard (May 23 2018 at 08:37):
that sort of thing
Kevin Buzzard (May 23 2018 at 08:37):
And Paulson wants to know what to do with this pot of euro money that he's sitting on
Kevin Buzzard (May 23 2018 at 08:39):
but we didn't talk much about that
Kevin Buzzard (May 23 2018 at 08:41):
but one of his post-docs, Angeliki Koutsoukou-Argyraki, is speaking at Imperial College London in a few weeks' time so perhaps I should have a think about this and talk to her
Kevin Buzzard (May 23 2018 at 08:41):
My impression is that Paulson wants to reach out to mathematicians but doesn't actually want to go and meet any, he has plenty of more important things to do
Kevin Buzzard (May 23 2018 at 08:41):
but he has people who can go and meet them for him
Kevin Buzzard (May 23 2018 at 08:42):
but he is very open to ideas of how to give money to mathematicians
Kevin Buzzard (May 23 2018 at 08:42):
and turn them to his way of thinking
Kevin Buzzard (May 23 2018 at 08:42):
and I can definitely work with that
Johan Commelin (May 23 2018 at 08:44):
This Haskell code producing human-readable proofs... was that from Tim Gowers?
Johan Commelin (May 23 2018 at 08:44):
He had such a project, but I think it was more like 2012 or something...
Patrick Massot (May 23 2018 at 08:44):
I'm pretty sure the best you could do now would be to document your journey towards that scheme milestone, then get Mario or Johannes to help you redoing it right, and document that second journey.
Patrick Massot (May 23 2018 at 08:44):
To me it seems way more useful than adding some more undergrad maths to some new proofs assistant
Patrick Massot (May 23 2018 at 08:46):
By the way, who is coming to Europe this summer in the end? I guess we all saw someone decided that ITP is not about maths (and it's not for lack of submissions). But maybe people still want to come?
Patrick Massot (May 23 2018 at 08:46):
There is also this http://www.uc.pt/en/congressos/thedu/thedu18 which is intriguing but there is no program yet
Mario Carneiro (May 23 2018 at 08:47):
I am going to Dagstuhl but not ITP this summer
Kevin Buzzard (May 23 2018 at 08:48):
Is the Dagstuhl the thing Assia is organising?
Patrick Massot (May 23 2018 at 08:48):
What is Dagstuhl?
Mario Carneiro (May 23 2018 at 08:48):
yes
Kevin Buzzard (May 23 2018 at 08:48):
Is that quite soon?
Kevin Buzzard (May 23 2018 at 08:48):
Last time I thought about that it seemed hopeless for me
Mario Carneiro (May 23 2018 at 08:48):
no, it's in August I think
Patrick Massot (May 23 2018 at 08:49):
Nooo, why August?
Patrick Massot (May 23 2018 at 08:49):
August doesn't exist
Kevin Buzzard (May 23 2018 at 08:49):
The dreaded month
Kevin Buzzard (May 23 2018 at 08:49):
if you're French
Kevin Buzzard (May 23 2018 at 08:49):
les vacances
Mario Carneiro (May 23 2018 at 08:49):
this https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=18341
Patrick Massot (May 23 2018 at 08:49):
Indeed, it's les vacances
Mario Carneiro (May 23 2018 at 08:50):
what's all this
Patrick Massot (May 23 2018 at 08:51):
In France attending a conference in mid-August pretty much automatically implies divorce
Sean Leather (May 23 2018 at 08:52):
Huh, so August in the Netherlands is not quite as bad as it sounds like August in France is, but I was always surprised how quiet it got.
Johan Commelin (May 23 2018 at 08:53):
Yes, August is the only month where we have decent weather... so we all leave the country (-;
Patrick Massot (May 23 2018 at 08:54):
I'm also pretty surprised this Dagstuhl thing was not advertised here before
Patrick Massot (May 23 2018 at 08:59):
Do you think this will be all about Coq and Isabelle, or there could be some room for Lean?
Mario Carneiro (May 23 2018 at 09:01):
Well, I'll be there...
Mario Carneiro (May 23 2018 at 09:01):
You should have seen when I went to represent metamath at a conference where no one's ever heard of it
Patrick Massot (May 23 2018 at 09:02):
I hope the case of Lean is different (metamath looks purely masochistic)
Mario Carneiro (May 23 2018 at 09:03):
It's really not as bad as it looks
Mario Carneiro (May 23 2018 at 09:03):
I would not have been so successful with it if it were not so ergonomic
Patrick Massot (May 23 2018 at 09:04):
@Sebastien Gouezel Did you discuss this conference with Assia?
Patrick Massot (May 23 2018 at 09:04):
Do you know more about it?
Patrick Massot (May 23 2018 at 09:06):
What about trying to gather either in London or Paris the week after Dagstuhl?
Patrick Massot (May 23 2018 at 09:07):
That week has much more existence
Sebastien Gouezel (May 23 2018 at 09:40):
Do you know more about it?
You mean the conference in August? I already had to negotiate with my wife to go to ICM, another conference this summer is completely impossible. So no, I have not discussed it with Assia.
Patrick Massot (May 23 2018 at 09:41):
I can believe that ICM is already too much
Patrick Massot (May 23 2018 at 09:42):
But Assia not advertising this conference to the only mathematician at her university interested in formal proof probably means this conference is not intended at all for mathematicians
Sebastien Gouezel (May 23 2018 at 09:43):
Yes, ICM is long, and far away. We considered going there with the family, but Rio is not the safest city in the world for a woman alone and three children...
Johannes Hölzl (May 23 2018 at 12:24):
I will be in Dagstuhl and at ITP in Oxford. Going to Paris or London would be easy for me.
Patrick Massot (May 23 2018 at 12:24):
Ah! Do you like schemes or manifolds?
Kevin Buzzard (May 23 2018 at 14:07):
A related question -- what about going to Paris _and_ London :-)
Assia Mahboubi (May 29 2018 at 11:46):
Hi, indeed I am (co)organizing this Dagstuhl stuff, with 3 colleagues: Andrej Bauer, Peter Lumsdaine and and Martin Escardo. Dagsthul is the CS's Oberwolfach so it is invitation only and the application (including the list of invitees) has been crafted a long time ago. Before I was even aware that you guys could be interested in this kind of event...
Last updated: Dec 20 2023 at 11:08 UTC