Zulip Chat Archive

Stream: general

Topic: function to pi type


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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:00):

use lambda?

view this post on Zulip Johan Commelin (May 23 2018 at 09:00):

O.o... lol

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:02):

Pi and structures are the only way of defining types

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:02):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:02):

or something

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:02):

Pi and inductive types

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:02):

lambda and mk

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:03):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:03):

Or is that abuse of language?

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

view this post on Zulip Sebastian Ullrich (May 23 2018 at 09:04):

Did you use nat? :stuck_out_tongue:

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

no, in the type theory literature that's common

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:04):

I mean

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:05):

actually I don't think I did use nat

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:05):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:05):

but they were all structures

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:05):

Sebastian's comment is interesting

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

There are tons of interesting inductive types beyond nat

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

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

the primitive recursive functions are obviously defined inductively

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

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

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

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

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

That answer was mostly a joke

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

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

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

I understand that Mario think Matiyesevich is math

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

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

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

unless you consider freely generated stuff to be inductive

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

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

it's obviously not all of math though

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

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

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

Essentially nobody in my department is interested in categories

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

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

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

but many are interested in schemes

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

constraints tend to be noninductive

view this post on Zulip Kenny Lau (May 23 2018 at 09:09):

Essentially nobody in my department is interested in categories

johannes nicaise is

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:10):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:10):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:11):

For most of us it's just a language

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

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

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:11):

I know

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:11):

doing that CS stuff

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

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

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

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

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

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

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

then some mathematicians would go "wooah"

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

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

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

but it is an extremely fashionable definition

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:13):

and a very delicate one

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:13):

And people like me prove basic lemmas about perfectoid spaces

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:13):

and get them published in good journals

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:13):

If you want to get a post-doc

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

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

then you have to impress the right people

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

but the right people in which discipline?

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

And there is a big disconnect here

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

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:14):

Langlands program pervades modern number theory and geometry

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

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

It places Fermat's Last Theorem in a bigger picture

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

So maybe we should start with fermat's last theorem

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

And you CS guys have made 0 progress with it

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

FLT is really old

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

it's all been done

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

not in lean

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

it would take a decade to formalise

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

by which time it would be even older

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

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

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

and nobody would care

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

but then it would be motivated

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:16):

and they said no

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:16):

_you_ would be motivated

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:16):

no mathematician would care

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

I think everyone wants motivation

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:16):

Defining a perfectoid space in Lean is 1000 times easier

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:16):

and _some_ mathematicians would care

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:16):

I mean, a non-trivial percentage would notice

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

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:17):

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:17):

So it still would be a major milestone

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:17):

because Peter Scholze is probably going to get a Fields Medal

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

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

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:17):

The reason FLT is impossible

view this post on Zulip Johan Commelin (May 23 2018 at 09:17):

Formalising the statement of the modularity theorem?

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:17):

is because you say that Cauchy Integral Formula is hard

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:18):

But that is a drop in an ocean of analysis

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:18):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:18):

which in every known proof of FLT is an essential prerequisite

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:18):

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

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

I like to formalize "essential prerequisites"

view this post on Zulip Johan Commelin (May 23 2018 at 09:19):

Statements or proofs?

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

both?

view this post on Zulip Johan Commelin (May 23 2018 at 09:19):

Great

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:19):

and no mathematician will care

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:19):

and after all that

view this post on Zulip Johan Commelin (May 23 2018 at 09:19):

Schemes are epsilon-th prerequisite for FLT

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:19):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:19):

and no mathematician will care

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:20):

because we proved it in the 1960s for SL_2

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:20):

like the odd order theorem

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:20):

and that's what we need

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:20):

There is your major obstacle for proving FLT

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:21):

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:21):

and you have seen how this turns out

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:21):

No

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:21):

it is about impressing people

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:21):

because that's where the jobs are

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:21):

and that's where the money is

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:21):

that's where the funding is

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:21):

that's how you get promotions

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:21):

that's how you get money to support your family

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

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

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:22):

but that won't happen

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

I don't think it need be so dichotomous

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

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

or even me

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

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

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

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

or kevin

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

Why not take a break from your formalizing basic gadgets

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

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

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

and formalize a fancy one with me

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:24):

and let's see the reaction

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:24):

Or

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:24):

if that's too fancy

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:24):

then formalize manifolds with Patrick

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:24):

because at least that's an important object

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:24):

(manifolds)

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:24):

and people in maths departments use them

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:25):

as opposed to Diophantine sets

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:25):

which are just some niche thing

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

which will get me publishing

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:25):

in your CS world

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:25):

That's the problem

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:25):

we seem to live in two different worlds

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

well we've all got mouths to feed

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:25):

You need your papers

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

and if the CS guys like the Diophantine set stuff

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

than that's what they're going to get

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

but the problem with this approach

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

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

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

is that the mathematicians will continue to not give a shit

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

Patrick, I was going to write something very short

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

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

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

but honestly let's face it

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

math journals don't care about that

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

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

for sure maths journals don't care

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

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

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

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

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

CS journals care, but they also care about CS things

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:28):

so I did something I thought was important

view this post on Zulip Johan Commelin (May 23 2018 at 09:28):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:28):

That can happen

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:28):

journals are not hard to start

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:29):

That was the story I was going to write

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:29):

except I can't imagine it's usable yet

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

Yes, because it's not done yet

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:30):

it is general frustration

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:30):

about the state of things

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:30):

that too

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:30):

but somehow the right people don't exist yet

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

If you would accept to play this game

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

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

I just have to make sure to stay somewhat on task

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

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

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

I think she's my hero

view this post on Zulip Johan Commelin (May 23 2018 at 09:33):

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

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

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:33):

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

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

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

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

Naive optimism is a very important math skill

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

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

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

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

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

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

I fear Hanoi is a bit too far for me

view this post on Zulip Andrew Ashworth (May 23 2018 at 09:44):

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

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

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

It's not 100% true

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

Since Assia is a counter-example for instance

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:52):

I want to bring computer formalized maths to mathematics departments

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:52):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:52):

both in terms of it making their lives better

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:54):

They are not missing that

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:54):

that - sign is not a mathematician's minus

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:54):

I see it and I see "-^*"

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:54):

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

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

actually it's a dot over, not a star

view this post on Zulip Andrew Ashworth (May 23 2018 at 09:55):

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:55):

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:55):

He completely changed fields

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:55):

In fact you could see this in his Cambridge talk

view this post on Zulip Johan Commelin (May 23 2018 at 09:55):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:56):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:56):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:56):

so he invented a new thing

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:56):

with yet another bloody definition of =

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

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:56):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:56):

and then oops

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:57):

who cares about Bloch-Kato any more

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:57):

and he explicitly said this in his Cambridge talk

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:57):

"So how is Bloch-Kato doing?"

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:57):

"Well, not very well"

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:57):

"I'm pretty sure it's right"

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:57):

"and nobody is working on that right now"

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:57):

exactly

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

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

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

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

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:58):

True

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

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:59):

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

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

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