Stream: general

Topic: function to pi type

Johan Commelin (May 23 2018 at 08:59):

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 (May 23 2018 at 08:59):

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

use lambda?

O.o... lol

Kevin Buzzard (May 23 2018 at 09:01):

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 (May 23 2018 at 09:02):

Pi and structures are the only way of defining types

Kevin Buzzard (May 23 2018 at 09:02):

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

or something

Kevin Buzzard (May 23 2018 at 09:02):

Pi and inductive types

lambda and mk

Kevin Buzzard (May 23 2018 at 09:03):

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

Kevin Buzzard (May 23 2018 at 09:03):

Or is that abuse of language?

Kevin Buzzard (May 23 2018 at 09:04):

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 (May 23 2018 at 09:04):

Did you use nat? :stuck_out_tongue:

Mario Carneiro (May 23 2018 at 09:04):

no, in the type theory literature that's common

I mean

Kevin Buzzard (May 23 2018 at 09:05):

actually I don't think I did use nat

Mario Carneiro (May 23 2018 at 09:05):

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

Kevin Buzzard (May 23 2018 at 09:05):

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

Kevin Buzzard (May 23 2018 at 09:05):

but they were all structures

Kevin Buzzard (May 23 2018 at 09:05):

Sebastian's comment is interesting

Mario Carneiro (May 23 2018 at 09:06):

There are tons of interesting inductive types beyond nat

Kevin Buzzard (May 23 2018 at 09:06):

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

Mario Carneiro (May 23 2018 at 09:06):

the primitive recursive functions are obviously defined inductively

Kevin Buzzard (May 23 2018 at 09:07):

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 (May 23 2018 at 09:07):

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

Mario Carneiro (May 23 2018 at 09:08):

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

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

That answer was mostly a joke

Mario Carneiro (May 23 2018 at 09:08):

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

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

I understand that Mario think Matiyesevich is math

Kevin Buzzard (May 23 2018 at 09:08):

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

Mario Carneiro (May 23 2018 at 09:08):

unless you consider freely generated stuff to be inductive

Kevin Buzzard (May 23 2018 at 09:09):

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

Mario Carneiro (May 23 2018 at 09:09):

it's obviously not all of math though

Kevin Buzzard (May 23 2018 at 09:09):

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

Kevin Buzzard (May 23 2018 at 09:09):

Essentially nobody in my department is interested in categories

Mario Carneiro (May 23 2018 at 09:09):

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

Kevin Buzzard (May 23 2018 at 09:09):

but many are interested in schemes

Mario Carneiro (May 23 2018 at 09:09):

constraints tend to be noninductive

Kenny Lau (May 23 2018 at 09:09):

Essentially nobody in my department is interested in categories

johannes nicaise is

Mario Carneiro (May 23 2018 at 09:10):

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

Kevin Buzzard (May 23 2018 at 09:10):

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

Kevin Buzzard (May 23 2018 at 09:10):

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

Kevin Buzzard (May 23 2018 at 09:11):

For most of us it's just a language

Patrick Massot (May 23 2018 at 09:11):

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

Mario Carneiro (May 23 2018 at 09:11):

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

I know

Mario Carneiro (May 23 2018 at 09:11):

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

Kevin Buzzard (May 23 2018 at 09:11):

doing that CS stuff

Kevin Buzzard (May 23 2018 at 09:12):

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

Patrick Massot (May 23 2018 at 09:12):

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

Kevin Buzzard (May 23 2018 at 09:12):

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

Kevin Buzzard (May 23 2018 at 09:12):

then some mathematicians would go "wooah"

Kevin Buzzard (May 23 2018 at 09:12):

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

Kevin Buzzard (May 23 2018 at 09:12):

but it is an extremely fashionable definition

Kevin Buzzard (May 23 2018 at 09:13):

and a very delicate one

Mario Carneiro (May 23 2018 at 09:13):

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

Kevin Buzzard (May 23 2018 at 09:13):

And people like me prove basic lemmas about perfectoid spaces

Kevin Buzzard (May 23 2018 at 09:13):

and get them published in good journals

Kevin Buzzard (May 23 2018 at 09:13):

If you want to get a post-doc

Johan Commelin (May 23 2018 at 09:13):

@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 (May 23 2018 at 09:14):

then you have to impress the right people

Kevin Buzzard (May 23 2018 at 09:14):

but the right people in which discipline?

Kevin Buzzard (May 23 2018 at 09:14):

And there is a big disconnect here

Johan Commelin (May 23 2018 at 09:14):

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

Mario Carneiro (May 23 2018 at 09:14):

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

Johan Commelin (May 23 2018 at 09:14):

Langlands program pervades modern number theory and geometry

Kevin Buzzard (May 23 2018 at 09:14):

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

Johan Commelin (May 23 2018 at 09:15):

It places Fermat's Last Theorem in a bigger picture

Kevin Buzzard (May 23 2018 at 09:15):

And you CS guys have made 0 progress with it

Kevin Buzzard (May 23 2018 at 09:15):

FLT is really old

Kevin Buzzard (May 23 2018 at 09:15):

it's all been done

not in lean

Kevin Buzzard (May 23 2018 at 09:15):

it would take a decade to formalise

Kevin Buzzard (May 23 2018 at 09:15):

by which time it would be even older

Johan Commelin (May 23 2018 at 09:15):

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

Kevin Buzzard (May 23 2018 at 09:15):

and nobody would care

Mario Carneiro (May 23 2018 at 09:16):

but then it would be motivated

Kevin Buzzard (May 23 2018 at 09:16):

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

and they said no

Kevin Buzzard (May 23 2018 at 09:16):

_you_ would be motivated

Kevin Buzzard (May 23 2018 at 09:16):

no mathematician would care

Mario Carneiro (May 23 2018 at 09:16):

I think everyone wants motivation

Kevin Buzzard (May 23 2018 at 09:16):

Defining a perfectoid space in Lean is 1000 times easier

Kevin Buzzard (May 23 2018 at 09:16):

and _some_ mathematicians would care

Kevin Buzzard (May 23 2018 at 09:16):

I mean, a non-trivial percentage would notice

Mario Carneiro (May 23 2018 at 09:17):

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

Johan Commelin (May 23 2018 at 09:17):

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

Johan Commelin (May 23 2018 at 09:17):

So it still would be a major milestone

Kevin Buzzard (May 23 2018 at 09:17):

because Peter Scholze is probably going to get a Fields Medal

Kevin Buzzard (May 23 2018 at 09:17):

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 (May 23 2018 at 09:17):

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

Johan Commelin (May 23 2018 at 09:17):

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

What do you mean with that?

Kevin Buzzard (May 23 2018 at 09:17):

The reason FLT is impossible

Johan Commelin (May 23 2018 at 09:17):

Formalising the statement of the modularity theorem?

Kevin Buzzard (May 23 2018 at 09:17):

is because you say that Cauchy Integral Formula is hard

Mario Carneiro (May 23 2018 at 09:18):

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

Kevin Buzzard (May 23 2018 at 09:18):

But that is a drop in an ocean of analysis

Kevin Buzzard (May 23 2018 at 09:18):

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

Kevin Buzzard (May 23 2018 at 09:18):

which in every known proof of FLT is an essential prerequisite

Johan Commelin (May 23 2018 at 09:18):

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

What do you mean with that?

Kevin Buzzard (May 23 2018 at 09:18):

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

Mario Carneiro (May 23 2018 at 09:18):

I like to formalize "essential prerequisites"

Johan Commelin (May 23 2018 at 09:19):

Statements or proofs?

both?

Great

Kevin Buzzard (May 23 2018 at 09:19):

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

Kevin Buzzard (May 23 2018 at 09:19):

and no mathematician will care

Kevin Buzzard (May 23 2018 at 09:19):

and after all that

Johan Commelin (May 23 2018 at 09:19):

Schemes are epsilon-th prerequisite for FLT

Kevin Buzzard (May 23 2018 at 09:19):

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

Kevin Buzzard (May 23 2018 at 09:19):

and no mathematician will care

Kevin Buzzard (May 23 2018 at 09:20):

because we proved it in the 1960s for SL_2

Kevin Buzzard (May 23 2018 at 09:20):

like the odd order theorem

Kevin Buzzard (May 23 2018 at 09:20):

and that's what we need

Kevin Buzzard (May 23 2018 at 09:20):

There is your major obstacle for proving FLT

Mario Carneiro (May 23 2018 at 09:20):

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 (May 23 2018 at 09:21):

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

Mario Carneiro (May 23 2018 at 09:21):

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

Kevin Buzzard (May 23 2018 at 09:21):

and you have seen how this turns out

No

Kevin Buzzard (May 23 2018 at 09:21):

because that's where the jobs are

Kevin Buzzard (May 23 2018 at 09:21):

and that's where the money is

Kevin Buzzard (May 23 2018 at 09:21):

that's where the funding is

Kevin Buzzard (May 23 2018 at 09:21):

that's how you get promotions

Mario Carneiro (May 23 2018 at 09:21):

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

Kevin Buzzard (May 23 2018 at 09:21):

that's how you get money to support your family

Andrew Ashworth (May 23 2018 at 09:21):

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

Mario Carneiro (May 23 2018 at 09:22):

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

Kevin Buzzard (May 23 2018 at 09:22):

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 (May 23 2018 at 09:22):

but that won't happen

Mario Carneiro (May 23 2018 at 09:22):

I don't think it need be so dichotomous

Johan Commelin (May 23 2018 at 09:22):

@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

or even me

Johan Commelin (May 23 2018 at 09:23):

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

Mario Carneiro (May 23 2018 at 09:23):

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

or kevin

Johan Commelin (May 23 2018 at 09:23):

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

Kevin Buzzard (May 23 2018 at 09:23):

and formalize a fancy one with me

Kevin Buzzard (May 23 2018 at 09:24):

and let's see the reaction

Or

Kevin Buzzard (May 23 2018 at 09:24):

if that's too fancy

Kevin Buzzard (May 23 2018 at 09:24):

then formalize manifolds with Patrick

Patrick Massot (May 23 2018 at 09:24):

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 (May 23 2018 at 09:24):

because at least that's an important object

(manifolds)

Kevin Buzzard (May 23 2018 at 09:24):

and people in maths departments use them

Kevin Buzzard (May 23 2018 at 09:25):

as opposed to Diophantine sets

Kevin Buzzard (May 23 2018 at 09:25):

which are just some niche thing

Mario Carneiro (May 23 2018 at 09:25):

which will get me publishing

Kevin Buzzard (May 23 2018 at 09:25):

That's the problem

Kevin Buzzard (May 23 2018 at 09:25):

we seem to live in two different worlds

Mario Carneiro (May 23 2018 at 09:25):

well we've all got mouths to feed

Kevin Buzzard (May 23 2018 at 09:26):

and if the CS guys like the Diophantine set stuff

Kevin Buzzard (May 23 2018 at 09:26):

than that's what they're going to get

Kevin Buzzard (May 23 2018 at 09:26):

but the problem with this approach

Johan Commelin (May 23 2018 at 09:26):

@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 (May 23 2018 at 09:26):

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

Kevin Buzzard (May 23 2018 at 09:26):

is that the mathematicians will continue to not give a shit

Kevin Buzzard (May 23 2018 at 09:26):

Patrick, I was going to write something very short

Mario Carneiro (May 23 2018 at 09:26):

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

Kevin Buzzard (May 23 2018 at 09:26):

but honestly let's face it

Mario Carneiro (May 23 2018 at 09:27):

math journals don't care about that

Kevin Buzzard (May 23 2018 at 09:27):

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 (May 23 2018 at 09:27):

for sure maths journals don't care

Patrick Massot (May 23 2018 at 09:27):

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

Kevin Buzzard (May 23 2018 at 09:27):

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

Mario Carneiro (May 23 2018 at 09:27):

CS journals care, but they also care about CS things

Kevin Buzzard (May 23 2018 at 09:27):

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

Kevin Buzzard (May 23 2018 at 09:28):

so I did something I thought was important

Johan Commelin (May 23 2018 at 09:28):

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

That can happen

Kevin Buzzard (May 23 2018 at 09:28):

journals are not hard to start

Patrick Massot (May 23 2018 at 09:29):

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 (May 23 2018 at 09:29):

That was the story I was going to write

Kevin Buzzard (May 23 2018 at 09:29):

except I can't imagine it's usable yet

Patrick Massot (May 23 2018 at 09:29):

Yes, because it's not done yet

Kevin Buzzard (May 23 2018 at 09:29):

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

Kevin Buzzard (May 23 2018 at 09:30):

it is general frustration

Patrick Massot (May 23 2018 at 09:30):

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

Patrick Massot (May 23 2018 at 09:30):

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

that too

Kevin Buzzard (May 23 2018 at 09:30):

but somehow the right people don't exist yet

Patrick Massot (May 23 2018 at 09:30):

If you would accept to play this game

Mario Carneiro (May 23 2018 at 09:30):

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

Mario Carneiro (May 23 2018 at 09:31):

I just have to make sure to stay somewhat on task

Patrick Massot (May 23 2018 at 09:31):

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

Mario Carneiro (May 23 2018 at 09:32):

I think she's my hero

Johan Commelin (May 23 2018 at 09:33):

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

Patrick Massot (May 23 2018 at 09:33):

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

Johan Commelin (May 23 2018 at 09:33):

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

Patrick Massot (May 23 2018 at 09:34):

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

Patrick Massot (May 23 2018 at 09:34):

Naive optimism is a very important math skill

Patrick Massot (May 23 2018 at 09:35):

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

Mario Carneiro (May 23 2018 at 09:36):

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

Patrick Massot (May 23 2018 at 09:37):

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

Mario Carneiro (May 23 2018 at 09:37):

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

Patrick Massot (May 23 2018 at 09:39):

I fear Hanoi is a bit too far for me

Andrew Ashworth (May 23 2018 at 09:44):

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

Andrew Ashworth (May 23 2018 at 09:45):

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 (May 23 2018 at 09:47):

It's not 100% true

Patrick Massot (May 23 2018 at 09:47):

Since Assia is a counter-example for instance

Andrew Ashworth (May 23 2018 at 09:49):

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 (May 23 2018 at 09:52):

I want to bring computer formalized maths to mathematics departments

Kevin Buzzard (May 23 2018 at 09:52):

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

Kevin Buzzard (May 23 2018 at 09:52):

both in terms of it making their lives better

Kevin Buzzard (May 23 2018 at 09:52):

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

Patrick Massot (May 23 2018 at 09:53):

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

Kevin Buzzard (May 23 2018 at 09:54):

They are not missing that

Kevin Buzzard (May 23 2018 at 09:54):

that - sign is not a mathematician's minus

Kevin Buzzard (May 23 2018 at 09:54):

I see it and I see "-^*"

Patrick Massot (May 23 2018 at 09:54):

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 (May 23 2018 at 09:54):

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

Mario Carneiro (May 23 2018 at 09:54):

actually it's a dot over, not a star

Andrew Ashworth (May 23 2018 at 09:55):

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

Johan Commelin (May 23 2018 at 09:55):

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

Johan Commelin (May 23 2018 at 09:55):

He completely changed fields

Kevin Buzzard (May 23 2018 at 09:55):

In fact you could see this in his Cambridge talk

Johan Commelin (May 23 2018 at 09:55):

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

Kevin Buzzard (May 23 2018 at 09:56):

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

Kevin Buzzard (May 23 2018 at 09:56):

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

Kevin Buzzard (May 23 2018 at 09:56):

so he invented a new thing

Kevin Buzzard (May 23 2018 at 09:56):

with yet another bloody definition of =

Mario Carneiro (May 23 2018 at 09:56):

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

Kevin Buzzard (May 23 2018 at 09:56):

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

and then oops

Kevin Buzzard (May 23 2018 at 09:57):

who cares about Bloch-Kato any more

Kevin Buzzard (May 23 2018 at 09:57):

and he explicitly said this in his Cambridge talk

Mario Carneiro (May 23 2018 at 09:57):

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

Kevin Buzzard (May 23 2018 at 09:57):

"So how is Bloch-Kato doing?"

Kevin Buzzard (May 23 2018 at 09:57):

"Well, not very well"

Kevin Buzzard (May 23 2018 at 09:57):

"I'm pretty sure it's right"

Kevin Buzzard (May 23 2018 at 09:57):

"and nobody is working on that right now"

exactly

Mario Carneiro (May 23 2018 at 09:57):

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

Mario Carneiro (May 23 2018 at 09:58):

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

Patrick Massot (May 23 2018 at 09:58):

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

True

Patrick Massot (May 23 2018 at 09:59):

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

Johan Commelin (May 23 2018 at 09:59):

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

Mario Carneiro (May 23 2018 at 09:59):

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

Johan Commelin (May 23 2018 at 09:59):

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

Last updated: May 09 2021 at 18:17 UTC