function to pi type

Stream: general

[Johan Commelin]

Newbie alert! I can't find anything in PIL or TPIL on how to construct a function to a Pi type. If I have Y : I \to Type and f : \Pi i, X \to Y i, how do I turn this into X \to (\Pi i, Y i)?

[Johan Commelin]

Context: I want to prove that the latter function is continuous if all the f i are continuous.

[Kevin Buzzard]

use lambda?

[Johan Commelin]

O.o... lol

[Kevin Buzzard]

example (I : Type) (X : Type) (Y : I → Type) (f : Π (i : I), X → Y i) : X → (Π i, Y i) := λ x, λ i, f i x

[Kevin Buzzard]

Pi and structures are the only way of defining types

[Kevin Buzzard]

and then lambda and { } are the only way of defining terms

[Kevin Buzzard]

or something

[Kevin Buzzard]

Pi and inductive types

[Kevin Buzzard]

lambda and mk

[Kevin Buzzard]

Can one say that lambda is some sort of a constructor for Pi types?

[Kevin Buzzard]

Or is that abuse of language?

[Kevin Buzzard]

Come to think of it, I am not sure I used a single inductive type in the whole scheme thing which wasn't a structure

[Sebastian Ullrich]

Did you use nat? :stuck_out_tongue:

[Mario Carneiro]

no, in the type theory literature that's common

[Kevin Buzzard]

I mean

[Kevin Buzzard]

actually I don't think I did use nat

[Mario Carneiro]

lambda is the intro rule for pi, and application is the elim form

[Kevin Buzzard]

but what I meant to say was that I rolled my own structures many times

[Kevin Buzzard]

but they were all structures

[Kevin Buzzard]

Sebastian's comment is interesting

[Mario Carneiro]

There are tons of interesting inductive types beyond nat

[Kevin Buzzard]

because how can a mathematician be doing anything if they're not using the basic math type, namely nat

[Mario Carneiro]

the primitive recursive functions are obviously defined inductively

[Kevin Buzzard]

but I think this maybe shows some disconnect between what the CS people think maths is, and what the maths people think it is

[Kevin Buzzard]

e.g. Mario saying "w00t I did some more Matiyesevich" and Patrick responding "when will you get back to math"

[Mario Carneiro]

I'm mentioning that because it's fresh on my mind

[Patrick Massot]

That answer was mostly a joke

[Mario Carneiro]

your scheme stuff is a bit too category-theoretic so have good examples

[Patrick Massot]

I understand that Mario think Matiyesevich is math

[Kevin Buzzard]

My scheme stuff is central to what a mathematician thinks that mathematics is

[Mario Carneiro]

unless you consider freely generated stuff to be inductive

[Kevin Buzzard]

and Patrick and I know well that most people in our departments would not have a clue about the Matiyesevich stuff

[Mario Carneiro]

it's obviously not all of math though

[Kevin Buzzard]

"a bit too category-theoretic" -- this is a very weird thing to day

[Kevin Buzzard]

Essentially nobody in my department is interested in categories

[Mario Carneiro]

it helps to look at more "concrete" areas, actual constructions and not constraints

[Kevin Buzzard]

but many are interested in schemes

[Mario Carneiro]

constraints tend to be noninductive

[Kenny Lau]

Essentially nobody in my department is interested in categories

johannes nicaise is

[Mario Carneiro]

so not "definition of scheme" but "X is a scheme"

[Kevin Buzzard]

Johannes knows what a category is, like most of us do

[Kevin Buzzard]

but Johannes does not study them in their own right, like most of us don't

[Kevin Buzzard]

For most of us it's just a language

[Patrick Massot]

Today's milestone is of type "X is a scheme"

[Mario Carneiro]

honestly I still have only the foggiest idea of what you guys actually do

[Kevin Buzzard]

I know

[Mario Carneiro]

I do all this math and you guys just say "oh that CS guy"

[Kevin Buzzard]

doing that CS stuff

[Kevin Buzzard]

This is one of the big reasons why this stuff isn't more popular

[Patrick Massot]

So let's gather at the end of August and discuss that

[Kevin Buzzard]

Mario, I honestly think that if we wrote the definition of a perfectoid space in Lean

[Kevin Buzzard]

then some mathematicians would go "wooah"

[Kevin Buzzard]

and your honest opinion might be "it's just a definition"

[Kevin Buzzard]

but it is an extremely fashionable definition

[Kevin Buzzard]

and a very delicate one

[Mario Carneiro]

I have no clue why I should care about perfectoid spaces, besides the societal stuff

[Kevin Buzzard]

And people like me prove basic lemmas about perfectoid spaces

[Kevin Buzzard]

and get them published in good journals

[Kevin Buzzard]

If you want to get a post-doc

[Johan Commelin]

@Mario Carneiro That's a very long story... but people are interested in them because they help us make progress on the Langlands programme

[Kevin Buzzard]

then you have to impress the right people

[Kevin Buzzard]

but the right people in which discipline?

[Kevin Buzzard]

And there is a big disconnect here

[Johan Commelin]

And people are interested in Langlands because... well, he just won the Abel prize for his impact on maths...

[Mario Carneiro]

I want to see it develop more inline with the history - starting concrete and tending towards abstraction as things get more complicated

[Johan Commelin]

Langlands program pervades modern number theory and geometry

[Kevin Buzzard]

The Langlands Philosophy is arguably one of the central problems in maths and definitely one of the central problems in number theory

[Johan Commelin]

It places Fermat's Last Theorem in a bigger picture

[Mario Carneiro]

So maybe we should start with fermat's last theorem

[Kevin Buzzard]

And you CS guys have made 0 progress with it

[Kevin Buzzard]

FLT is really old

[Kevin Buzzard]

it's all been done

[Mario Carneiro]

not in lean

[Kevin Buzzard]

it would take a decade to formalise

[Kevin Buzzard]

by which time it would be even older

[Johan Commelin]

@Mario Carneiro Yes, but to do FLT, you have to define a scheme

[Kevin Buzzard]

and nobody would care

[Mario Carneiro]

but then it would be motivated

[Kevin Buzzard]

Proof that nobody would care: I went around and asked a bunch of people if they would care

[Kevin Buzzard]

and they said no

[Kevin Buzzard]

_you_ would be motivated

[Kevin Buzzard]

no mathematician would care

[Mario Carneiro]

I think everyone wants motivation

[Kevin Buzzard]

Defining a perfectoid space in Lean is 1000 times easier

[Kevin Buzzard]

and _some_ mathematicians would care

[Kevin Buzzard]

I mean, a non-trivial percentage would notice

[Mario Carneiro]

Even just setting up a foundation for FLT would be tremendously satisfying for me

[Johan Commelin]

Well, if FLT is formalised, then certainly lots of other modern stuff will be easily formalisable

[Johan Commelin]

So it still would be a major milestone

[Kevin Buzzard]

because Peter Scholze is probably going to get a Fields Medal

[Kevin Buzzard]

Even just setting up a foundation for FLT would be tremendously satisfying for me

Well then you need to start caring about schemes

[Mario Carneiro]

I'm all about the library building, making impossible goals feasible

[Johan Commelin]

Even just setting up a foundation for FLT would be tremendously satisfying for me

What do you mean with that?

[Kevin Buzzard]

The reason FLT is impossible

[Johan Commelin]

Formalising the statement of the modularity theorem?

[Kevin Buzzard]

is because you say that Cauchy Integral Formula is hard

[Mario Carneiro]

FLT is in a whole language of its own, let's get that theory

[Kevin Buzzard]

But that is a drop in an ocean of analysis

[Kevin Buzzard]

all of which needs to be done to prove the trace formula

[Kevin Buzzard]

which in every known proof of FLT is an essential prerequisite

[Johan Commelin]

FLT is in a whole language of its own, let's get that theory

What do you mean with that?

[Kevin Buzzard]

Mario -- like Johan I don't understand what you're saying

[Mario Carneiro]

I like to formalize "essential prerequisites"

[Johan Commelin]

Statements or proofs?

[Mario Carneiro]

both?

[Johan Commelin]

Great

[Kevin Buzzard]

Well you can spend two years formalising Cauchy Integral Formula and then basic stuff about integration on complex manifolds

[Kevin Buzzard]

and no mathematician will care

[Kevin Buzzard]

and after all that

[Johan Commelin]

Schemes are epsilon-th prerequisite for FLT

[Kevin Buzzard]

you will proudly be able to formalise the statement of the trace formula

[Kevin Buzzard]

and no mathematician will care

[Kevin Buzzard]

because we proved it in the 1960s for SL_2

[Kevin Buzzard]

like the odd order theorem

[Kevin Buzzard]

and that's what we need

[Kevin Buzzard]

There is your major obstacle for proving FLT

[Mario Carneiro]

and then you will have a demo where you show people how to work with basic calculus and it won't be a barrier anymore

[Kevin Buzzard]

And then 10 years later we have a proof of a 35-year-old theorem

[Mario Carneiro]

it's not about impressing people with the statements, it's about making regular stuff pain free

[Kevin Buzzard]

and you have seen how this turns out

[Kevin Buzzard]

No

[Kevin Buzzard]

it is about impressing people

[Kevin Buzzard]

because that's where the jobs are

[Kevin Buzzard]

and that's where the money is

[Kevin Buzzard]

that's where the funding is

[Kevin Buzzard]

that's how you get promotions

[Mario Carneiro]

It's not what they want, it's what they need

[Kevin Buzzard]

that's how you get money to support your family

[Andrew Ashworth]

i'm curious if MSR has any work on this; I know they want to prove certain properties of encryption protocols

[Mario Carneiro]

so you have to split your effort between flashy stuff and foundations

[Kevin Buzzard]

I absolutely agree that in a perfect world we should all just drop what we're doing and prove the trace formula and tell mathematicians to stop producing more maths

[Kevin Buzzard]

but that won't happen

[Mario Carneiro]

I don't think it need be so dichotomous

[Johan Commelin]

@Mario Carneiro FLT will never be formalised if it takes one of the leading number theorists of our time over 3 months to formalise the definition of the most basic gadget in the proof

[Kevin Buzzard]

or even me

[Johan Commelin]

Really, defining a scheme takes less then an hour in "Introduction to algebraic geometry"

[Mario Carneiro]

Right, so I will formalize the most basic gadgets and then leading number theorists won't have to

[Mario Carneiro]

or kevin

[Kevin Buzzard]

Why not take a break from your formalizing basic gadgets

[Johan Commelin]

@Mario Carneiro They will get hopelessly stuck on whatever comes after the basics

[Kevin Buzzard]

and formalize a fancy one with me

[Kevin Buzzard]

and let's see the reaction

[Kevin Buzzard]

Or

[Kevin Buzzard]

if that's too fancy

[Kevin Buzzard]

then formalize manifolds with Patrick

[Patrick Massot]

Kevin did formalize the basic gadget. Now you have the opportunity to do it right, and I'm sure that would be immensely instructive

[Kevin Buzzard]

because at least that's an important object

[Kevin Buzzard]

(manifolds)

[Kevin Buzzard]

and people in maths departments use them

[Kevin Buzzard]

as opposed to Diophantine sets

[Kevin Buzzard]

which are just some niche thing

[Mario Carneiro]

which will get me publishing

[Kevin Buzzard]

in your CS world

[Kevin Buzzard]

That's the problem

[Kevin Buzzard]

we seem to live in two different worlds

[Mario Carneiro]

well we've all got mouths to feed

[Kevin Buzzard]

You need your papers

[Kevin Buzzard]

and if the CS guys like the Diophantine set stuff

[Kevin Buzzard]

than that's what they're going to get

[Kevin Buzzard]

but the problem with this approach

[Johan Commelin]

@Mario Carneiro You have incredible skills. But atm mathematicians are really unable to use Lean, (except for a couple weirdo nerds like Kevin, Patrick, Scott and me). We really hope that you will help us build the bridge that the regular mathematicians need.

[Patrick Massot]

How is it possible that formalizing Diophantine sets could give you a paper but formalize schemes couldn't?

[Kevin Buzzard]

is that the mathematicians will continue to not give a shit

[Kevin Buzzard]

Patrick, I was going to write something very short

[Mario Carneiro]

I can't publish in a math journal, unless I stop formalizing

[Kevin Buzzard]

but honestly let's face it

[Mario Carneiro]

math journals don't care about that

[Kevin Buzzard]

whatever would I do with a two page paper saying "I wrote down a trivial definition, it took three months, here are some of the interesting problems I ran into"

[Kevin Buzzard]

for sure maths journals don't care

[Patrick Massot]

Why not publishing about formalization of schemes in a CS journal?

[Kevin Buzzard]

and from a CS point of view all I did was formalise a definition

[Mario Carneiro]

CS journals care, but they also care about CS things

[Kevin Buzzard]

I am in a privileged position that I can just do what I like

[Kevin Buzzard]

so I did something I thought was important

[Johan Commelin]

Right, so we need a new journal "Formalisations in Geometry and Number Theory"

[Kevin Buzzard]

That can happen

[Kevin Buzzard]

journals are not hard to start

[Patrick Massot]

As I wrote earlier, I think the really interesting thing to write about would be the whole process starting with an optimistic mathematician knowing nothing about DTT and ending with a usable formalization

[Kevin Buzzard]

That was the story I was going to write

[Kevin Buzzard]

except I can't imagine it's usable yet

[Patrick Massot]

Yes, because it's not done yet

[Kevin Buzzard]

Mario -- I hope you understand that none of this is an implicit criticism of what you do

[Kevin Buzzard]

it is general frustration

[Patrick Massot]

It lacks the stage where Mario or Johannes enters the game seriously

[Kevin Buzzard]

about the state of things

[Patrick Massot]

It's not only frustration, it's also excitement about what could be

[Kevin Buzzard]

that too

[Kevin Buzzard]

but somehow the right people don't exist yet

[Patrick Massot]

If you would accept to play this game

[Mario Carneiro]

The thing is, the things I enjoy are useful to others, but not really publishable results for the most part

[Mario Carneiro]

I just have to make sure to stay somewhat on task

[Patrick Massot]

How did Assia got her job then? I think she always formalized math

[Mario Carneiro]

I think she's my hero

[Johan Commelin]

Well, and there is Tom Hales of course. He knows everything about FLT and about formalisation.

[Patrick Massot]

Then why don't you start reading that scheme repository?

[Johan Commelin]

Still he did not formalise any algebraic geometry or anything in the direction of Langlands yet

[Patrick Massot]

I guess Hales knows too much, this prevents him from enjoying Kevin's optimism

[Patrick Massot]

Naive optimism is a very important math skill

[Patrick Massot]

I don't think I was ever able to prove anything without first hugely underestimating the difficulty

[Mario Carneiro]

Also Johannes and I will be working at the university of Hanoi with Tom on a lean summer school

[Patrick Massot]

I think your hero would write "Scheme theory done right in Lean"

[Mario Carneiro]

As I understand it many of the folks involved in Flyspeck are there, so it should be interesting

[Patrick Massot]

I fear Hanoi is a bit too far for me

[Andrew Ashworth]

ooh, Flyspeck looks interesting! So they proved the optimal packing of balls in 3d space

[Andrew Ashworth]

Please don't pressure Mario too hard :) For his future career prospects, all the money in formal verification comes from the large software companies

[Patrick Massot]

It's not 100% true

[Patrick Massot]

Since Assia is a counter-example for instance

[Andrew Ashworth]

I'm not aware of very many other mathematicians outside of Assia who get to work on computer formalized math... whereas, Intel, Amazon, Microsoft, Facebook etc. all have teams of people who do this. Not to mention the smaller companies like Galois and others who do contract work in the field

[Kevin Buzzard]

I want to bring computer formalized maths to mathematics departments

[Kevin Buzzard]

because I think mathematicians don't know what they're missing

[Kevin Buzzard]

both in terms of it making their lives better

[Kevin Buzzard]

and in terms of the fact that some of their arguments are incomplete and they need to be told

[Patrick Massot]

I know what they are missing: a - b + b may or may not be equal to a

[Kevin Buzzard]

They are not missing that

[Kevin Buzzard]

that - sign is not a mathematician's minus

[Kevin Buzzard]

I see it and I see "-^*"

[Patrick Massot]

Formalized math in maths departments may be a dream too far away. But we only need two INRIA positions: one for Mario and one for Johannes

[Kevin Buzzard]

with the footnote "this is a different minus, don't expect it to be sensible"

[Mario Carneiro]

actually it's a dot over, not a star

[Andrew Ashworth]

Not even a Field's medalist in Vovoedsky could get mathematicians interested in DTT...

[Johan Commelin]

Because he didn't formalise any AG (= Algebraic Geometry)

[Johan Commelin]

He completely changed fields

[Kevin Buzzard]

In fact you could see this in his Cambridge talk

[Johan Commelin]

I don't think he even formalised the definition of a scheme in all those years

[Kevin Buzzard]

He got interested in formal proof verification because he was worried about bugs in his proofs

[Kevin Buzzard]

but then he decided that DTT or whatever wasn't right for him

[Kevin Buzzard]

so he invented a new thing

[Kevin Buzzard]

with yet another bloody definition of =

[Mario Carneiro]

When you do HoTT though, everything is "more" than what's written

[Kevin Buzzard]

and then all of a sudden there were lots of interesting questions

[Kevin Buzzard]

and then oops

[Kevin Buzzard]

who cares about Bloch-Kato any more

[Kevin Buzzard]

and he explicitly said this in his Cambridge talk

[Mario Carneiro]

and you get distracted by all the homotopy implications of your definition and never get around to the original goal

[Kevin Buzzard]

"So how is Bloch-Kato doing?"

[Kevin Buzzard]

"Well, not very well"

[Kevin Buzzard]

"I'm pretty sure it's right"

[Kevin Buzzard]

"and nobody is working on that right now"

[Kevin Buzzard]

exactly

[Mario Carneiro]

formalizing a scheme in HoTT feels like the wrong application of a tool

[Mario Carneiro]

because you have no interest in the HoTT stuff, it's just a classical definition

[Patrick Massot]

Recently I heard someone claiming a proof of this Simpson conjecture that was missing in order to fix that broken Voevodsky paper that started it all

[Johan Commelin]

True

[Patrick Massot]

https://ncatlab.org/nlab/show/Simpson%27s+conjecture

[Johan Commelin]

@Mario Carneiro Unless HoTT helps you to turn math-trivial stuff into formally-trivial stuff.

[Mario Carneiro]

I like lean because it's not trying to be "more" like this, it's exactly what you are trying to say

[Johan Commelin]

I think Voevodsky thought very hard about transport of structure. And that led him to HoTT