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

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):

https://github.com/kbuzzard/lean-stacks-project/blob/d2f64a23d8e6347bde488de0b0a93be1b72f18d6/src/tag00E8.lean#L145

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

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

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)?

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

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):

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):

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):

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?

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

if you're French

les vacances

Patrick Massot (May 23 2018 at 08:49):

Indeed, it's les vacances

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: May 10 2021 at 07:15 UTC