Zulip Chat Archive

Stream: maths

Topic: foundations of mathematics


view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:20):

I spent some time over the last couple of days learning about Voevodsky's work in type theory. I found this paper https://arxiv.org/abs/1711.01477 by Dan Grayson quite illuminating.

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:20):

quite high

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:20):

It seems to me that univalent foundations is similar to, but not the same as, DTT

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:20):

a = b is not a Prop in univalent foundations

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:21):

In fact there seems to me to be no impredicative Prop universe in univalent foundations

view this post on Zulip Patrick Massot (Apr 10 2018 at 08:21):

What happened to your project of documenting what's in mathlib?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:21):

there are just some universes, and a Prop is basically defined to be a subsingleton

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:22):

But the claim is the same as in Lean -- "we can use this set-up as a way of doing all of maths"

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:22):

kenny would love hott

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:22):

kenny would love hott

nope

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:22):

One major weakness (possibly only temporary) is that the model you're supposed to carry around is that a type can be thought of as a topological space

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:23):

but apparently they can't construct the n-sphere from the axioms

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:23):

so they add n-spheres as new inductive types

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:23):

and then they can't prove the theory is consistent

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:23):

This does not bode well, as far as I can see.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:23):

kenny would love hott

nope

are you a fair-weather constructivist

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:23):

I also re-watched Voevodsky's Newton Institute talk from last yeat

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:23):

year

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:23):

abuse of topology

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:24):

and his discussion about how he tried to persuade Suslin to re-prove some theorem of his constructively

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:24):

because Voevodsky wanted to prove an old theorem of Voevodsky constructively in this univalent foundations way

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:25):

but my impression was that Suslin had no interest in the question (perhaps unsurprisingly, as I know essentially 0 mathematicians who care about constructive maths)

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:25):

1

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:25):

and it seemed that Voevodsky was losing interest in the whole project of checking the proof anyway (or perhaps he was stuck)

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:25):

Alessio Corto

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:25):

Alessio Corti

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:26):

sure

view this post on Zulip Patrick Massot (Apr 10 2018 at 08:26):

To me it settles the question: HoTT is constructive ⇒ I don't care

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:26):

I think Voevodsky is something else

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:26):

I think HoTT might be a third thing

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:26):

I'm not sure though

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:27):

Is Univalent Foundations = HoTT? I'm not so sure

view this post on Zulip Patrick Massot (Apr 10 2018 at 08:27):

More precisely: it's constructive ⇒ I think it's irrelevant to most mathematics

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:27):

I completely agree.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:27):

So here are some questions.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:28):

We know that Lean will allow classical logic, and to be quite frank if it didn't allow it then I definitely would not be here.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:28):

I should say Lean 3, because at some point one has to talk about what Lean 2 was

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:29):

Univalent Foundations seems to have been implemented in Coq, but there are lots of rules about commands in Coq which you are _not allowed to use_ in Univalent Foundations

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:29):

e.g. you are not allowed to make new inductive types

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:29):

you have to stick to the ones they made in the core files

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:29):

But I should get to the point.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:29):

If I am interested in mathematics, done in classical logic

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:30):

then what are my options for doing this in type theory?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:30):

DTT I know, because Lean 3

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:30):

HoTT?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:30):

Univalent Foundations?

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:30):

Voevodsky is high

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:30):

And if there is more than one option, why should I choose Lean 3?

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:30):

that settles it

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:30):

Voevodsky is dead :-(

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:31):

oh rip

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:31):

there are very few popular dtt languages; you've already listed two, coq and lean, and there is also agda and idris

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:32):

i think ats might also be based on dtt

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:32):

basically the only other contender is not based on dtt at all, which is isabelle

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:33):

how is she doing

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:34):

It is worth noting that both Agda and Idris are primarily programming languages. Unlike Lean and Coq.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:35):

isabelle is quite popular amongst mathematicians

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:35):

because it ain't constructive?

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:35):

because they press Sledgehammer butan'

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:35):

What are Isabelle's foundations?

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:36):

Isabelle is a metalanguage, you can instantiate it with whatever you feel like. Isabelle/HOL is the most popular.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:36):

i know little of isabelle. but my impression is most people work in set theory

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:37):

This is what Hales used for Kepler, right?

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:37):

one should make a proof-assistant based on ZFC

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:37):

As in ZF(C)? Mmm, I've always thought it's mostly just HOL.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:37):

that's already been done 30 years ago

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:37):

who?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:37):

Apparently proof assistants based on ZFC are hard to use

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:38):

I think Mario told me this

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:38):

the original big one was called mizar

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:38):

Apparently proof assistants based on ZFC are hard to use

another reason why ZFC is BS

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:38):

I believe Isabelle/ZFC is also a thing.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:38):

i recall sebastian gouzel was also slightly annoyed with isabelle

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:38):

something about it being impossible to define the adeles

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:38):

(whatever they may be)(

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:39):

What do you mean by impossible?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:39):

Kenny is supposed to be defining the adeles in Lean

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:39):

once he's finished revising his mechanics

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:39):

discussion of the adeles is beyond my pay grade

view this post on Zulip Sean Leather (Apr 10 2018 at 08:39):

@Andrew Ashworth:

i think ats might also be based on dtt

Not quite

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:40):

There is certainly no obstruction to defining the adeles in Lean

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:40):

There is once you don't have dependent types (a'la Isabelle).

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:40):

yes, iirc he said that was a major draw for him to work in dtt

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:40):

discussion of the adeles is beyond my pay grade

it isn't quite hard to understand if you start simple, i.e. start with Q

view this post on Zulip Patrick Massot (Apr 10 2018 at 08:40):

https://gitter.im/leanprover_public/Lobby?at=5a2daedfffa3e379191e9195

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:41):

Kenny, the adeles of a general number field K are just (adeles of Q) tensor_Q K

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:41):

and because you did tensor product

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:41):

you can do adeles for a general number field

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:41):

wonderful

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:42):

The adeles are an easy exercise given what we have

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:42):

isabelle and coq currently have ::quite:: an advantage in library size

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:42):

quite

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:42):

leaving aside isabelle, why would you use lean over coq? mostly for nicer unicode syntax

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:42):

But we seem to have a proof that isabelle is not suitable for all of mathematics?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:42):

Lean > Coq -- because tactics

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:43):

however if you wanted to jump straight into doing research mathematics, you can't in lean because mathlib is far smaller than its coq competitors

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:43):

far smaller than it is coq competitors

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:43):

and I think that nicer unicode syntax, whilst this might just be superficial for CS people, will I think be important to undergraduate mathematicians

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:43):

Coq > Lean because of existing tactics. Lean > Coq because of the way you write tactics.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:44):

But I am playing the long game

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:44):

So I choose Lean. However this thread was basically my attempt to review this choice.

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:44):

If you're playing the very long game, it might still be the case Coq > Lean, Ltac2 is coming.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:44):

If I can understand the claim that "Isabelle can't do the adeles" then we can cross Isabelle off the list

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:45):

But what about HoTT?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:45):

And what about UniMath?

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:45):

hott is not ready for anything, it is a subject of research

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:45):

And this does not apply to DTT

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:45):

because Coq

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:45):

let's do things over NBG

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:46):

or just second order peano arithmetic

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:46):

The original univalence axiom is not constructive. There's cubical type theory extension thereof tho: https://arxiv.org/abs/1611.02108

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:46):

dtt without any funny additions has been proven sound

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:46):

sound!

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:46):

sound in what?

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:46):

as in you can do useful things with it and not summon false from anywhere

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:46):

how do you even define sound

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:46):

by "proven sound" you mean "relative to ZFC + existence of infinitely many inaccessible cardinals" right?

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:46):

@Kenny Lau Funny you should say that. My table currently contains "Subsystems of second order arithmetic".

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:46):

You can't prove that anything is sound, in some sense

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:47):

exactly

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:47):

without assuming consistency of some less-likely-to-be-sound system

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:48):

forget about the reals

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:48):

just do peano arithmetic

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:48):

and then embed ZFC within

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:48):

and then Goedel encode everything.

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:48):

and then you can do the reals

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:49):

i think for undergraduates who are not trying to do research mathematics, lean is nicer for reading and writing tactics (though i doubt they will get around to writing tactics)

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:49):

Actually, Coq has much nicer tactic-description syntax still.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:49):

coq is the winner if you're trying to make something that will be around for years

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:50):

it has been around for decades

view this post on Zulip Kenny Lau (Apr 10 2018 at 08:50):

feit thompson e.g.

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:50):

You can pattern match on goals themselves for example. There's no obscure monad with arbitrary pexpr transforming functions.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:51):

i think writing tactics is beyond most mathematician's interest

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:51):

realistically speaking

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:51):

Realistically speaking, using Lean is beyond most mathematician's interest :P.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:51):

also true

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:51):

i think this has a sadder part though

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:52):

using Lean is beyond most CS peoeple interest as well

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:52):

well, most cs majors would rather have a tooth pulled than work with something that reminds them of their undergraduate discrete math course

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:54):

most people studying CS want to be "programmers", there's no clear distinction between CS and software engineering in academia, for worse or worse

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:54):

I agree about tactics. For now.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:54):

But I am going to make mathematicians interested in Lean.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:55):

if you split the two cleanly then academic CS may as well be in the math department along with the statisticians

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:55):

and logicians

view this post on Zulip Patrick Massot (Apr 10 2018 at 08:55):

But I am going to make mathematicians interested in Lean.

Then we need more documentation, for instance your old project of describing mathlib

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:56):

oh yeah sorry Patrick I didn't respond to your earlier question

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:56):

I am still trying to figure out all the finite stuff

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:56):

but multiset.lean is so long

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:57):

My blog post about induction was just some consequence of me trying to understand finite stuff

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:57):

For mathematicians, finite sets are so important and foundational

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:57):

and I found them very hard to do in DTT

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:57):

but I am slowly getting on top of them

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 08:57):

@Andrew Ashworth well we then need to communicate better what to expect in a CS course at least... it is as you said, tooth extraction wins over discrete math for many students I teach...

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:58):

My middle child is a budding CS student and he was moaning about discrete maths only 2 days ago

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 08:58):

surely he knows better than to moan about maths to you, haha

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:58):

:-)

view this post on Zulip Patrick Massot (Apr 10 2018 at 08:59):

I know I'm always writing the same thing, but did you read that Coq bigoperator paper?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:59):

I was reading it yesterday

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:59):

I learnt some stuff

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:59):

For example I didn't really know how to prove that sum from 0 to n of f(i) equalled sum from 0 to n of f(n-i)

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 08:59):

but I can now see a nice way of doing it using bigoperators

view this post on Zulip Sean Leather (Apr 10 2018 at 09:00):

Discrete math was one of my favorite undergrad courses.

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 09:01):

I teach Java to students that had compulsory discrete math one semester prior. They think I'm evil when I want them to, and I quote, "remember what properties equivalence relations have"... :-\

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:03):

In summary then, apparently HoTT isn't ready, UniMath I am still unsure about, Isabelle has problems with adeles, Mizar didn't catch on for some reason, so there's only DTT left?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:04):

And if it turns out that Coq > Lean then I just switch to Coq

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:04):

that is a bonus. if lean ever dies everything you've learnt moves easily over to coq

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:05):

Can I write a regular expression which turns all my Lean proofs into Coq proofs?

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:05):

that's a little ambitious :)

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:05):

Oh Ok

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:05):

I don't know what you CS guys can do

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 09:06):

I don't think it's a completely ridiculous idea.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:06):

i mean, it's theoretically possible to write a transpiler. but who would do the work?

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:07):

Lean advantages over Coq are not only about unicode. You also get better overall ergonomics. And, most of all, less constructive stuff.

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:07):

And much better documentation

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 09:07):

How is less constructive stuff a good thing?!

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:07):

It's a good thing for mathematics, not for everything

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:07):

well.. lean, instead of having less constructive stuff, just has _less_ stuff :)

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:08):

From what I understand, in Coq you need to spend more energy fighting constructivism

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:08):

In Dan Grayson's article he argues that constructive maths is better than normal maths because constructive maths is a generalisation of normal maths

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:08):

I was like "..."

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

I should tell all the group theorists I know to move into monoid theory

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:09):

Exactly what I was about to write

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:09):

let's all do monoids!

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

actually let's just do set theory

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

who cares about structure

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

we have the classification theorem already

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

each one bijects with a unique cardinal

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

so off we go

view this post on Zulip Moses Schönfinkel (Apr 10 2018 at 09:10):

this is surprisingly reminiscent of static vs dynamic typing discussion

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:10):

also, unimath is basically hott

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:10):

unimath is dtt + univalence

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

What is this documentation comment Patrick?

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:10):

and then a bunch of mathematics

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

I thought Coq had some big chunky tomes

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:10):

like, actual math, like i recall seeing a construction of the reals using dedekind cuts

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:11):

so unimath is basically mathlib + univalence

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:11):

equality is not a prop in unimath

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:11):

apparently

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:11):

equality in unimath seems more like \equiv in Lean

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:12):

if i knew more homotopy theory i'd feel more eager to say things about hott :)

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:14):

What is this documentation comment Patrick?

Coq has no documentation targeting mathematicians. TPIL is written for us, and beats anything I've seen about Coq by a very wide margin.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:26):

yes, the big three textbooks for coq are: software foundations, certified programming with dependent types, and coq'art. ssreflect also has a good manual here. notice all but the last is focused towards programmers...

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:33):

SSReflect manual is clearly going in the right direction compared to the other three, but it's still much harder to read that TPIL (I tried reading it before switching to Lean).

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:06):

I thought that Coq also had some useful introductory tutorials. But I agree with Patrick that TPIL is a very good read for mathematicians.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:07):

Patrick -- I was going to write something else for mathematicians, where I enter tactic mode on page 1 and basically never leave, and also on page 1 I do mathematics rather than goofing around with logic, doing basic mathematical proofs of familiar statements like stuff involving congruences right from square 1. I show them the tactics they need and we go from there.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:08):

I still think that term mode is too hard for mathematicians. You clearly have a programming background. I am guessing that you were happy with lambda notation for functions before you started reading these docs.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:08):

I would like to suppress lambda notation for as long as possible.

view this post on Zulip Patrick Massot (Apr 10 2018 at 10:09):

I agree wholeheartedly with all those goals

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:12):

OK! Thanks for your opinion, I genuinely value it.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:13):

We are both in the same sort of boat, trying to read books written for computer scientists with in some sense an "amateur" background (with me rather more amateurish than you when it comes to computing) but I really want to appeal to people who know no CS at all.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:20):

Back to the point -- does anyone here know if one can do classical mathematics in UniMath?

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 10:27):

I think so. https://github.com/HoTT/HoTT/issues/299

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 10:41):

speaking of, i linked this a long time ago, but here you can see a comparison of the most popular proof languages

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 10:41):

http://www.cs.ru.nl/~freek/100/

view this post on Zulip Simon Hudon (Apr 10 2018 at 16:13):

yes, the big three textbooks for coq are: software foundations, certified programming with dependent types, and coq'art. ssreflect also has a good manual here. notice all but the last is focused towards programmers...

I think that suggests @Patrick Massot has the right idea: if you want documentation for mathematicians, we need actual mathematicians to do it.

view this post on Zulip Patrick Massot (Apr 10 2018 at 16:17):

I don't if you count Avigad as mathematician but TPIL comes very close to what we want. You only to unemphasize term mode and put more math examples.

view this post on Zulip Simon Hudon (Apr 10 2018 at 16:23):

Right. What I meant is that building a theorem prover is something done by programmers so it kind of colors what they'll use the prover for in the documentation.

view this post on Zulip Simon Hudon (Apr 10 2018 at 16:27):

That's the curious difference between a prover and an accounting software. In accounting software, you do it for / with accountants / people who want to do accounting. With a prover, I have a feeling you start one when you need a prover that does stuff that the other provers don't do. You're kind of the first user of the prover so you assume the other users will want the prover for the same reason. Not that I built a prover with more than 1.5 users but ...

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 16:33):

I don't if you count Avigad as mathematician but TPIL comes very close to what we want. You only to unemphasize term mode and put more math examples.

term mode is not the enemy! i feel like if one wants to get anything done, you'll end up needing to know both modes
personally my favorite code style for math is the isabelle style, as seen https://github.com/sgouezel/mathlib/blob/d4836822a625677b9f292e26fcafb4870bbf9f91/order/conditionally_complete_lattice.lean

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:38):

Term mode is not the enemy. But for a mathematician there are many things which you have to learn in order to work this sort of language, and term mode is somehow one of the more obscure things. Let's give them time to wrestle with how to steer this thing whilst they're proving that the square root of 2 is irrational, or whatever, in tactic mode, before telling them that lambda is no longer supposed to mean a real number.

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 16:43):

if logic and proof (jeremy's other textbook) was fully worked out in lean 3, is that something you'd be looking for?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:47):

That's less Lean and less tactic mode!

view this post on Zulip Patrick Massot (Apr 10 2018 at 16:47):

I didn't write "completely remove term mode" but "unemphasize" (I don't know if this word exists but I hope what I mean is clear)

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 16:48):

ah, true. only 50% of logic and proof is lean

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:48):

I know exactly what I want, and I'm going to write it myself using Jeremy's cool org mode solution for generating books

view this post on Zulip Patrick Massot (Apr 10 2018 at 16:48):

I'd be happy to help in any way

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 16:49):

very awesome, i think everyone here would love to peek at it as you write it

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 16:49):

at least i would, i read all your blog posts, hah

view this post on Zulip Simon Hudon (Apr 10 2018 at 16:50):

@Kevin Buzzard I think he moved from org-mode to Restructured Text, didn't he?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:51):

In some sense the main question I have for Patrick is how to write a book which has maths like R[1/f]R[1/f] and lean stuff like this all coloured in correctly.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:51):

Simon I was basing my org claim on this

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:51):

https://github.com/leanprover/mkleanbook

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:52):

and the fact that the files were called blah.org

view this post on Zulip Patrick Massot (Apr 10 2018 at 16:52):

This is not how TPIL is currently produced

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:52):

You must be right

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:52):

do you know how it's currently done?

view this post on Zulip Patrick Massot (Apr 10 2018 at 16:53):

Sphinx

view this post on Zulip Patrick Massot (Apr 10 2018 at 16:53):

https://github.com/leanprover/theorem_proving_in_lean

view this post on Zulip Patrick Massot (Apr 10 2018 at 16:53):

scroll down to README

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 16:53):

that said, there is nothing wrong with mkleanbook, the issue was other people didn't want to use emacs

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:54):

what about getting things inmathsmodein maths mode?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 16:54):

(although perhaps not regular sentences, they can stay in non maths mode)

view this post on Zulip Simon Hudon (Apr 10 2018 at 17:27):

Do you mean that you would format Lean code in math mode? I'd really like to see that

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 17:53):

I mean I want to write maths and Lean code (at different times)

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 17:54):

Ideally the maths I write would look as good as LaTeX and the Lean would be coloured in correctly

view this post on Zulip Simon Hudon (Apr 10 2018 at 17:55):

Ah ok! I think the setup they have for Lean documents should allow that

view this post on Zulip Simon Hudon (Apr 10 2018 at 17:57):

I'm soon going to give Pandoc a try. I heard good things about it and it looks easier to set up than Sphinx

view this post on Zulip Simon Hudon (Apr 10 2018 at 17:59):

Ideally, I'd like to get to a point where I don't have to switch between writing and checking Lean and writing and checking documentation.

view this post on Zulip Mario Carneiro (Apr 10 2018 at 20:03):

One major weakness (possibly only temporary) is that the model you're supposed to carry around is that a type can be thought of as a topological space
but apparently they can't construct the n-sphere from the axioms
so they add n-spheres as new inductive types
and then they can't prove the theory is consistent
This does not bode well, as far as I can see.

As far as I am aware, HoTT + all the HITs people care about, including S^n and quotients and things, is known consistent because of the existence of simplicial set models and such. The unknown consistency claim here may be particular to Univalent Foundations, I'm not sure.

view this post on Zulip Mario Carneiro (Apr 10 2018 at 20:06):

Is Univalent Foundations = HoTT? I'm not so sure

I think Univalent Foundations = HoTT + Propositional resizing, which means that everything you can prove is a proposition lives in the lowest universe. This is similar to Lean's Prop universe, but in Lean you can't prove that something lives in Prop, it either is or isn't by virtue of the form of the expression. Regular HoTT does not have this resizing rule, so there are "more propositions" in higher universes, which talk about correspondingly large objects.

view this post on Zulip Mario Carneiro (Apr 10 2018 at 20:08):

If I am interested in mathematics, done in classical logic
then what are my options for doing this in type theory?

I think this is the wrong question. You can do mathematics in just about any system above a certain minimum threshold of complexity, which is somewhere around second order PA. It just gets less convenient as you remove features

view this post on Zulip Mario Carneiro (Apr 10 2018 at 20:14):

I believe Isabelle/ZFC is also a thing.

Pretty much all Isabelle work is done in Isabelle/HOL. Metamath is similar in that it is a general framework which allows you to define DTT, HOL, ZFC, PA or anything else, but 99% of the actual theorem proving work has gone into the ZFC database.

Apparently proof assistants based on ZFC are hard to use
I think Mario told me this

I'm not 100% clear on this, because I hear conflicting messages, but this is the usual line:

  • ZFC based stuff is hard to use in proof automation because there isn't much information on what is what, which helps in relevance filtering and eliminating proof steps that are not well typed
  • Type theory based stuff is hard for proof automation because keeping track of all the types is hard, and all the major tools are built in FOL with one big FOL universe, i.e. ZFC (or smaller FOL systems like first order equational theories, PA, etc.)

view this post on Zulip Mario Carneiro (Apr 10 2018 at 20:18):

If you're playing the very long game, it might still be the case Coq > Lean, Ltac2 is coming.

If you are playing a sufficiently long game, the best bet doesn't exist yet

dtt without any funny additions has been proven sound

DTT with inductive types, quotients and proof irrelevance is also sound, courtesy of yours truly

view this post on Zulip Mario Carneiro (Apr 10 2018 at 20:20):

I am still trying to figure out all the finite stuff
but multiset.lean is so long

You don't need to read multiset.lean that carefully. The easy version is: it's lists up to permutation, with all the list functions lifted to multiset. All the lemmas are exactly what you would expect, given the definitions.

view this post on Zulip Mario Carneiro (Apr 10 2018 at 20:22):

i mean, it's theoretically possible to write a transpiler. but who would do the work?

I would, if I understood Coq's metatheory as well as I do Lean's. Since they were not nearly so careful with their kernel as Lean has been, I don't know if I will find the acceptable Gallina terms written up anywhere that isn't an approximation or out of date

view this post on Zulip Mario Carneiro (Apr 10 2018 at 20:28):

equality in unimath seems more like \equiv in Lean

This is exactly the right idea. However, there is something you really need to pay attention to which I think you have missed and are using to get a "free lunch" in your conception of HoTT: equality (the type constructor) is not the same as definitional equality. In Lean this isn't that big a deal because of proof irrelevance, but you absolutely cannot hold the view that one thing is as good as an equal thing when doing HoTT. In particular, it will not save you from your "up to equivalence" problems in the other thread, but I will discuss this more there.

view this post on Zulip Mario Carneiro (Apr 10 2018 at 20:49):

I still think that term mode is too hard for mathematicians. You clearly have a programming background. I am guessing that you were happy with lambda notation for functions before you started reading these docs.
I would like to suppress lambda notation for as long as possible.

I don't think this is a good idea. The idea of a lambda itself, a function giving a result, is quite integral to mathematics and it's a surprise they haven't picked up the notation already (or something isomorphic, like x \in A |-> b(x)).

If you want to write a tactic-centric lean tutorial, I would suggest to begin with a brief overview of the terms of the language, i.e. lambda, application, constants and variables, make sure they understand what a bound variable is, then move on with some statement along the lines "writing these terms directly is cumbersome, so here's a language for quickly constructing terms that is designed more for ease of use". You don't need to mention the Isar-inspired terms like match and have and show until later if you want, but the core type theory should be at least briefly described.

view this post on Zulip Scott Morrison (Apr 10 2018 at 23:06):

It is a good point that mathematicians know perfectly well about lambdas, they just write them $x \mapsto f(x)$.


Last updated: May 09 2021 at 11:09 UTC