Zulip Chat Archive

Stream: Lean for the curious mathematician 2020

Topic: aim


Johan Commelin (May 13 2020 at 17:50):

What is the aim?

Reid Barton (May 13 2020 at 17:50):

Did you have an aim before?

Johan Commelin (May 13 2020 at 17:50):

I don't want to be the BDFL... so I'm open to suggestions.

Johan Commelin (May 13 2020 at 17:51):

This is what I wrote before https://math.commelin.net/2020/lftcm/

Patrick Massot (May 13 2020 at 17:51):

My understanding was the aim is propaganda

Patrick Massot (May 13 2020 at 17:51):

Attracting more users.

Patrick Massot (May 13 2020 at 17:51):

Have a look at the first two graph at https://leanprover-community.github.io/mathlib_stats.html. What do you see?

Jalex Stark (May 13 2020 at 17:51):

An aim: getting more math done.
One goal is to increase the expected "surface area" of math formalized in lean, say marked out to one year from now, where by "surface area" I mean places where someone can pick up and start making new contributions, ideally without having to spend much time filling in "boring prerequisites"

Jalex Stark (May 13 2020 at 17:52):

who is a user?

Jalex Stark (May 13 2020 at 17:52):

someone who spends their time doing math and for whom Lean has changed the way they think about it?

Jalex Stark (May 13 2020 at 17:52):

someone who spends their time writing Lean code?

Patrick Massot (May 13 2020 at 17:53):

Looking at these graphs I see linear growth. That's good enough to get undergrad math covered within the next two years. But proof assistant useful for mathematicians need exponential growth.

Patrick Massot (May 13 2020 at 17:54):

It means we need to double the number of Yurys and Sébastien each year (without loosing the previous ones like we lost Mario and Johannes).

Mario Carneiro (May 13 2020 at 17:54):

hey...

Jalex Stark (May 13 2020 at 17:54):

i also don't know what "lost mario" means

Patrick Massot (May 13 2020 at 17:55):

This question is answered in the last two graphs on the same page

Mario Carneiro (May 13 2020 at 17:55):

I don't contribute as many PR's as I used to because I am working on other things

Jalex Stark (May 13 2020 at 17:55):

ah okay, so measured in number of PRs

Patrick Massot (May 13 2020 at 17:55):

Sure, I never wrote "Mario stopped working"

Mario Carneiro (May 13 2020 at 17:56):

(Actually I never really wrote a lot of PR's, when I was active I would just push to master)

Jalex Stark (May 13 2020 at 17:56):

an aim: getting more funding
I guess this means "make our goals be the same as things that grant agencies like"

Patrick Massot (May 13 2020 at 17:56):

If we kept Mario and Johannes and added Sébastien and Yury the first two graphs would look exponential

Patrick Massot (May 13 2020 at 17:57):

But course we also need people to move around, so let's triple the number of Marios each year and loose some along the road

Patrick Massot (May 13 2020 at 17:58):

Anway, dreaming is useless here. Let's say the aim is to have more people having fun explaining math to their computers

Jalex Stark (May 13 2020 at 17:58):

so we're trying to attract like, young grad students and late undergrads who are very strong but haven't solidly committed to a particular path?

Jalex Stark (May 13 2020 at 17:58):

Patrick Massot said:

Anway, dreaming is useless here. Let's say the aim is to have more people having fun explaining math to their computers

mm i still think we need a story for why this particular avenue adds to our goal more than just hanging out on zulip

Mario Carneiro (May 13 2020 at 17:59):

I'm happy to "just hang out" in virtual conference form

Patrick Massot (May 13 2020 at 17:59):

Why only young people? Why not getting a couple more dinosaurs like me, or even a couple of primordial soup species like Kevin?

Johan Commelin (May 13 2020 at 17:59):

Another aim might be to show "older" mathematicians how this software could useful for an "intro to proofs" course.

Mario Carneiro (May 13 2020 at 18:00):

there is never any shortage of topics to talk about, especially if we give people assignments to give short talks

Patrick Massot (May 13 2020 at 18:00):

Is it Kevin's let's-wait-for-them-to-die strategy again?

Jalex Stark (May 13 2020 at 18:00):

Patrick Massot said:

Why only young people? Why not getting a couple more dinosaurs like me, or even a couple of primordial soup species like Kevin?

oh sure, I just think they're harder to target,
but obviously that's a personal bias I know more people in the young category

Patrick Massot (May 13 2020 at 18:02):

Jalex Stark said:

mm i still think we need a story for why this particular avenue adds to our goal more than just hanging out on zulip

Johan suggested some kinds of talks. And we don't use discord or twitch on Zulip usually

Reid Barton (May 13 2020 at 18:02):

So in general there is a progression "Lean user → mathlib contributor → mathlib maintainer → go off and write your own theorem prover" that we can always try to add more people into.

Johan Commelin (May 13 2020 at 18:03):

Reid, I've never told anyone about my theorem prover. But how is yours doing?

Reid Barton (May 13 2020 at 18:03):

It's still in the design phase

Patrick Massot (May 13 2020 at 18:03):

Yeah, I also have a design: I think about something that would be nice, and the proof assistant proves it.

Jalex Stark (May 13 2020 at 18:05):

the best proof assistant design is that all your sorries are sent to a central server, and if they hang out unsolved for long enough, undergrads can come in and close them for course credit

Patrick Massot (May 13 2020 at 18:05):

We used to have a much better version of this.

Jalex Stark (May 13 2020 at 18:05):

I think we need to get significantly better at interaction between Lean and external oracles before that dream

Patrick Massot (May 13 2020 at 18:06):

But then I moved on to creating his own proof assistant.

Mario Carneiro (May 13 2020 at 18:06):

No one sends me interesting problems anymore

Jalex Stark (May 13 2020 at 18:06):

well i don't know, that system is not capable of doing 100 times as many goals which are each 10 times as easy

Jalex Stark (May 13 2020 at 18:07):

both because each problem has overhead and because the person-oracle is limited by their interest

Patrick Massot (May 13 2020 at 18:07):

Mario Carneiro said:

No one sends me interesting problems anymore

Is that nlinarith doing the same as in Coq already?

Mario Carneiro (May 13 2020 at 18:07):

Hey it happened didn't it

Mario Carneiro (May 13 2020 at 18:08):

the next stage is figuring out how the heck linarith works

Patrick Massot (May 13 2020 at 18:08):

What an interesting problem!

Mario Carneiro (May 13 2020 at 18:09):

Jalex Stark said:

the best proof assistant design is that all your sorries are sent to a central server, and if they hang out unsolved for long enough, undergrads can come in and close them for course credit

One drawback of this architecture is that you tend to get pretty crappy proofs

Mario Carneiro (May 13 2020 at 18:09):

unless you also outsource proof optimization problems

Mario Carneiro (May 13 2020 at 18:09):

Personally, I find proof optimization to be the most interesting task

Jalex Stark (May 13 2020 at 18:11):

i think closing a sorry gets you a number of points that's some function of "how fast your code runs" and "how fast the previous fastest was"

Jalex Stark (May 13 2020 at 18:11):

and maybe the first person to close it gets like 1/3 of the total possible points

Mario Carneiro (May 13 2020 at 18:11):

this sounds way better than codewars

Patrick Massot (May 13 2020 at 18:11):

That's not the kind of optimization Mario is talking about

Mario Carneiro (May 13 2020 at 18:11):

I mean optimization in all senses (some of which contradict others)

Jalex Stark (May 13 2020 at 18:12):

yeah for sure, you want some notion of "evaluation of how useful / good this proof is" which eventually you get by some kind of expert-voting

Jalex Stark (May 13 2020 at 18:12):

but to jumpstart things you want to fall back on an explicit heuristic

Bhavik Mehta (May 13 2020 at 18:13):

Maybe outsource evaluation to the undergrads as well

Patrick Massot (May 13 2020 at 18:13):

We may have drifted a bit here

Jalex Stark (May 13 2020 at 18:14):

I've thought a decent amount about this, PM me if you want to discuss privately

Jalex Stark (May 13 2020 at 18:15):

(and let's let this thread serve its original purpose)

Mario Carneiro (May 13 2020 at 18:15):

or move to another stream/topic?

Jalex Stark (May 13 2020 at 18:15):

go ahead, though I think my enthusiasm for discussing such half-formed ideas in the open is low

Jalex Stark (May 13 2020 at 18:16):

So @Patrick Massot, do you think we should be maximizing something like "expected number of PRs to mathlib six months from now?"

Patrick Massot (May 13 2020 at 18:17):

This is only one aspect.

Patrick Massot (May 13 2020 at 18:17):

And dinner is calling

Reid Barton (May 13 2020 at 18:17):

Another goal is the sort of PR/public awareness that a lot of Kevin's talks are aimed at: it's good to let the "generic mathematician" know what we are doing even if we don't expect them to end up making PRs to mathlib.

Reid Barton (May 13 2020 at 18:17):

And there's only so much one can say in a 1-hour talk, or indeed a 17-minute talk on perfectoid spaces.

Reid Barton (May 13 2020 at 18:18):

A few years ago I found it quite hard to even find out things like "what math has been formalized?"

Jalex Stark (May 13 2020 at 18:18):

is the PR/public awareness similar to maximizing "expected amount of grant funding available 1 year from now for theorem proving in lean"

Patrick Massot (May 13 2020 at 18:19):

It's broader

Reid Barton (May 13 2020 at 18:19):

Yes, that is certainly an aspect of it.

Jalex Stark (May 13 2020 at 18:19):

is it more like maximizing "expected number of practicing mathematicians who know such-and-such basics of the Lean community project"?
where the basics are the things we list on the community webpage?

Mario Carneiro (May 13 2020 at 18:20):

also formal theorem proving in general; lean might be their first exposure to the field so there is some groundwork to be laid as well

Mario Carneiro (May 13 2020 at 18:21):

is there a guest list?

Johan Commelin (May 13 2020 at 18:22):

I have a list with 10 ~ 13 email addresses of people who expressed interest. They are all active on Zulip.

Mario Carneiro (May 13 2020 at 18:22):

are there any curious mathematicians on the list?

Johan Commelin (May 13 2020 at 18:22):

Not really

Johan Commelin (May 13 2020 at 18:23):

As in, all of them already use Lean

Johan Commelin (May 13 2020 at 18:23):

But remember that I had crappy restraints before going online. Like a room with place for <18 people.

Johan Commelin (May 13 2020 at 18:24):

So it was clear that there wouldn't be many "total newbies"

Mario Carneiro (May 13 2020 at 18:24):

you may want to do another advertising run

Johan Commelin (May 13 2020 at 18:26):

Yep certainly. But after the dust settled down of the current brainstorming session.

Patrick Massot (May 13 2020 at 18:54):

Mario Carneiro said:

are there any curious mathematicians on the list?

I think Damien Thomine registered. He has done very few Lean.

Johan Commelin (May 13 2020 at 18:54):

Oh, that's right

Patrick Massot (May 13 2020 at 18:54):

And Antoine Chambert-Loir was interested, although he couldn't make it. He also has done very few Lean, and maybe he could join us

Patrick Massot (May 13 2020 at 18:55):

I think there are enough curious mathematicians to have a virtual meeting that is really for curious mathematicians, not bored undergrads. Bored undergrads should having something too, but they already have Kevin's stuff.

Patrick Massot (May 13 2020 at 18:56):

(Kevin's stuff is totally unclear to me, but that's a different topic)

Johan Commelin (May 13 2020 at 18:57):

Patrick Massot said:

And Antoine Chambert-Loir was interested, although he couldn't make it. He also has done very few Lean, and maybe he could join us

Yup, and Daniel Litt, and Emily Riehl, David Holmes, Simon Pepin-Lehalleur... those are all mathematicians who have "flirted" with Lean. I would love to spark some more/new enthousiasm again...
(Of those, Emily is by far the closest to a user.)

Johan Commelin (May 13 2020 at 18:58):

Ooh, and Peter Bruin.
(Just collecting names, in case we want to send announcements to specific people at some point.)

Patrick Massot (May 13 2020 at 18:59):

After attending her talk last week, I fear Emily won't want to invest time in a proof assistant neglecting HoTT.

Mario Carneiro (May 13 2020 at 19:00):

What I would really like to get the HoTT-minded mathematicians into is formalizing the foundations of HoTT in a theorem prover

Mario Carneiro (May 13 2020 at 19:01):

that is, the "external" viewpoint of HoTT, which seems to be what all the papers are about

Reid Barton (May 13 2020 at 19:01):

I have thought about this but then the first question is whether to do the whole thing constructively or not

Bhavik Mehta (May 13 2020 at 19:02):

I would argue a strong yes

Mario Carneiro (May 13 2020 at 19:02):

I am 100% okay with saying "of course not" to that, but perhaps the target audience might not want to hear that

Jalex Stark (May 13 2020 at 19:02):

Mario Carneiro said:

What I would really like to get the HoTT-minded mathematicians into is formalizing the foundations of HoTT in a theorem prover

Is this similar to what a logician might call "constructing a model of HoTT"?

Mario Carneiro (May 13 2020 at 19:02):

yes

Jalex Stark (May 13 2020 at 19:02):

so then inside the model you'll have all of the constructiveness you want?

Mario Carneiro (May 13 2020 at 19:03):

exactly

Reid Barton (May 13 2020 at 19:03):

Of course my biases are also to do everything classically but indeed most other people interested in formalizing these things would also want to have it done constructively.

Jalex Stark (May 13 2020 at 19:03):

Seems like an obvious yes to me too, in the sense that if the API exists then the HoTT-person should not care about the implementation

Mario Carneiro (May 13 2020 at 19:03):

asking for constructiveness at the meta level is irrelevant

Reid Barton (May 13 2020 at 19:03):

I don't understand which option is "yes" or "no" any more.

Jalex Stark (May 13 2020 at 19:03):

and then other people coming in afterwards could do it constructively if they want

Jalex Stark (May 13 2020 at 19:04):

I think Mario and I think you should nonconstructively build a model of HoTT

Patrick Massot (May 13 2020 at 19:04):

You know there is a Type theory stream, right?

Jalex Stark (May 13 2020 at 19:05):

https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/How.20to.20get.20HoTT.20people.20into.20Lean/near/197460897

Jalex Stark (May 13 2020 at 19:05):

thanks patrick for the diligent moderation

Jalex Stark (May 13 2020 at 19:05):

i think we got here by thinking about which specific people we are likely to attract to this event

Jalex Stark (May 13 2020 at 19:06):

it seems like people in the community know a decent number of specific, Lean-curious, postdoc-aged people.
So we may be able to cater the whole event to people of that age / mathematical maturity

Jalex Stark (May 13 2020 at 19:07):

(I guess I know at least one such person that I'll try to bring to this event)

Jalex Stark (May 13 2020 at 19:07):

So should we advertise for "early career researchers"?

Patrick Massot (May 13 2020 at 19:08):

What about "mathematician"?

Patrick Massot (May 13 2020 at 19:08):

Sorry for insisting that some old people still move a bit

Jalex Stark (May 13 2020 at 19:08):

sorry, I only meant to put a lower bound

Jalex Stark (May 13 2020 at 19:08):

"early career researchers and professors"?

Jalex Stark (May 13 2020 at 19:09):

I don't mean to bikeshed on the name of this group of people

Jalex Stark (May 13 2020 at 19:09):

I just want to nail down who they are

Jalex Stark (May 13 2020 at 19:10):

they're people that have their own interesting research programs, have an existing body of work and idea for how to extend that work for years to come?

Jalex Stark (May 13 2020 at 19:11):

@Patrick Massot does "mathematician" mean "postdoc or professor" to you, or does it mean something broader?

Dima Pasechnik (Jun 29 2020 at 09:50):

I got a notification about this event from a colleague at Oxford Maths Institute, @Aurelio Carlucci

Johan Commelin (Jun 29 2020 at 10:05):

@Dima Pasechnik See also the website at https://leanprover-community.github.io/lftcm2020/

Dima Pasechnik (Jun 29 2020 at 10:08):

Johan Commelin said:

Dima Pasechnik See also the website at https://leanprover-community.github.io/lftcm2020/

sure, I came here via the website, in fact :-)

Johan Commelin (Jun 29 2020 at 10:09):

Ok, good. That means it's working :wink:


Last updated: Dec 20 2023 at 11:08 UTC