Zulip Chat Archive

Stream: maths

Topic: ALEXANDRIA: Proof for the Working Mathematician


view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 15 2018 at 12:09):

Wow, those are big claims (-;

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:18):

I mean, I guess he didn't say _exactly_ that...

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 15 2018 at 12:21):

Such a shame to do this in Isabelle

view this post on Zulip Patrick Massot (May 15 2018 at 12:21):

He should have come here

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:21):

My impression is that he is really into the idea of formal proofs being readable.

view this post on Zulip Patrick Massot (May 15 2018 at 12:21):

As far as I can see there is no obstruction to having readable proofs in Lean

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:22):

I mean, human-readable source code

view this post on Zulip Patrick Massot (May 15 2018 at 12:22):

It's only Mario and Johannes don't like them

view this post on Zulip Patrick Massot (May 15 2018 at 12:22):

The sledgehammer thing is much more serious issue of course

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:23):

intros a Ha

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:24):

Maybe I should be writing intros a proof_that_a_is_in_X

view this post on Zulip Patrick Massot (May 15 2018 at 12:24):

I often try to do that

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:26):

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

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:26):

"I follow my nose, cases, rw, apply, cases, exact, intro, split, cases, apply, exact"

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:27):

and voila, Spec(R) is compact

view this post on Zulip Patrick Massot (May 15 2018 at 12:27):

I don't think it would be hard to make it easier to read

view this post on Zulip Patrick Massot (May 15 2018 at 12:27):

You already have a couple of explicit have

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:27):

I agree

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:28):

it was certainly easy to write :-)

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:28):

but my point is that I didn't

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:28):

make it easy to read

view this post on Zulip Patrick Massot (May 15 2018 at 12:28):

You could add a few more, maybe with some suffices

view this post on Zulip Patrick Massot (May 15 2018 at 12:31):

Why "quasi-compact" if you prove compactness?

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:33):

I thought that this was the French's fault?

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:34):

In the UK, compact := every cover has a finite subcover. In France it's Hausdorff + ...

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:34):

but alg geom is a French subject

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:34):

because schemes are typically not Hausdorff, it's quasi-compact

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 15 2018 at 12:41):

Oh, I understand: you mean mathlib's definition of compactness is the broken one (without Haussdorff)?

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:41):

right

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:41):

it's only broken because of your cultural upbringing

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:41):

One could instead regard it as a translation issue

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:41):

English "compact" := French quasi-compact

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (May 15 2018 at 12:42):

well I did point out that my proof was just 50 lines of intro, apply, exact ;-)

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 15 2018 at 12:54):

But then, you forget saying Haussdorff half the time!

view this post on Zulip Kevin Buzzard (May 15 2018 at 13:19):

He's using type class inference

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:26):

Did you get any insights with the ALEXANDRIA / Peter Koepke lecture person today?

yesterday

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:27):

That was an interesting day

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:31):

And after that there was a long discussion

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:32):

for over 2 hours

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:32):

where we just talked about life and where all this was going

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:33):

Their system is called SAD

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:34):

what his point was, was that the proof script is genuinely human-readable

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:34):

and everyone dreamt about having all 1st and 2nd year UG maths in their system

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:35):

but I think that only I have a coherent strategy for making this happen

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:35):

i.e. getting 1st and 2nd year UGs to put it into the system themselves

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:35):

and we all moaned about how the Cauchy Integral Formula was hard

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:36):

and Paulson even had an anecdote about it

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:36):

having translated Harrison's proof from (something) into (something)

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:36):

maybe from HOL light into Isabelle?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:37):

that sort of thing

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:39):

but we didn't talk much about that

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:41):

but he has people who can go and meet them for him

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:42):

but he is very open to ideas of how to give money to mathematicians

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:42):

and turn them to his way of thinking

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:42):

and I can definitely work with that

view this post on Zulip Johan Commelin (May 23 2018 at 08:44):

This Haskell code producing human-readable proofs... was that from Tim Gowers?

view this post on Zulip Johan Commelin (May 23 2018 at 08:44):

He had such a project, but I think it was more like 2012 or something...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 23 2018 at 08:47):

I am going to Dagstuhl but not ITP this summer

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:48):

Is the Dagstuhl the thing Assia is organising?

view this post on Zulip Patrick Massot (May 23 2018 at 08:48):

What is Dagstuhl?

view this post on Zulip Mario Carneiro (May 23 2018 at 08:48):

yes

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:48):

Is that quite soon?

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:48):

Last time I thought about that it seemed hopeless for me

view this post on Zulip Mario Carneiro (May 23 2018 at 08:48):

no, it's in August I think

view this post on Zulip Patrick Massot (May 23 2018 at 08:49):

Nooo, why August?

view this post on Zulip Patrick Massot (May 23 2018 at 08:49):

August doesn't exist

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:49):

The dreaded month

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:49):

if you're French

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:49):

les vacances

view this post on Zulip Mario Carneiro (May 23 2018 at 08:49):

this https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=18341

view this post on Zulip Patrick Massot (May 23 2018 at 08:49):

Indeed, it's les vacances

view this post on Zulip Mario Carneiro (May 23 2018 at 08:50):

what's all this

view this post on Zulip Patrick Massot (May 23 2018 at 08:51):

In France attending a conference in mid-August pretty much automatically implies divorce

view this post on Zulip 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.

view this post on Zulip 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 (-;

view this post on Zulip Patrick Massot (May 23 2018 at 08:54):

I'm also pretty surprised this Dagstuhl thing was not advertised here before

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 23 2018 at 09:01):

Well, I'll be there...

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 23 2018 at 09:02):

I hope the case of Lean is different (metamath looks purely masochistic)

view this post on Zulip Mario Carneiro (May 23 2018 at 09:03):

It's really not as bad as it looks

view this post on Zulip Mario Carneiro (May 23 2018 at 09:03):

I would not have been so successful with it if it were not so ergonomic

view this post on Zulip Patrick Massot (May 23 2018 at 09:04):

@Sebastien Gouezel Did you discuss this conference with Assia?

view this post on Zulip Patrick Massot (May 23 2018 at 09:04):

Do you know more about it?

view this post on Zulip Patrick Massot (May 23 2018 at 09:06):

What about trying to gather either in London or Paris the week after Dagstuhl?

view this post on Zulip Patrick Massot (May 23 2018 at 09:07):

That week has much more existence

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 23 2018 at 09:41):

I can believe that ICM is already too much

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 23 2018 at 12:24):

Ah! Do you like schemes or manifolds?

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:07):

A related question -- what about going to Paris _and_ London :-)

view this post on Zulip 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