aim

Stream: Lean for the curious mathematician 2020

[Johan Commelin]

What is the aim?

[Reid Barton]

Did you have an aim before?

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

My understanding was the aim is propaganda

[Patrick Massot]

Attracting more users.

[Patrick Massot]

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

[Jalex Stark]

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]

who is a user?

[Jalex Stark]

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

[Jalex Stark]

someone who spends their time writing Lean code?

[Patrick Massot]

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]

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]

hey...

[Jalex Stark]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Jalex Stark]

ah okay, so measured in number of PRs

[Patrick Massot]

Sure, I never wrote "Mario stopped working"

[Mario Carneiro]

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

[Jalex Stark]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Jalex Stark]

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]

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]

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

[Patrick Massot]

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]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Jalex Stark]

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]

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]

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]

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

[Reid Barton]

It's still in the design phase

[Patrick Massot]

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

[Jalex Stark]

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]

We used to have a much better version of this.

[Jalex Stark]

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

[Patrick Massot]

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

[Mario Carneiro]

No one sends me interesting problems anymore

[Jalex Stark]

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]

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

[Patrick Massot]

Mario Carneiro said:

No one sends me interesting problems anymore

Is that nlinarith doing the same as in Coq already?

[Mario Carneiro]

Hey it happened didn't it

[Mario Carneiro]

the next stage is figuring out how the heck linarith works

[Patrick Massot]

What an interesting problem!

[Mario Carneiro]

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]

unless you also outsource proof optimization problems

[Mario Carneiro]

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

[Jalex Stark]

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]

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

[Mario Carneiro]

this sounds way better than codewars

[Patrick Massot]

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

[Mario Carneiro]

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

[Jalex Stark]

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]

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

[Bhavik Mehta]

Maybe outsource evaluation to the undergrads as well

[Patrick Massot]

We may have drifted a bit here

[Jalex Stark]

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

[Jalex Stark]

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

[Mario Carneiro]

or move to another stream/topic?

[Jalex Stark]

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

[Jalex Stark]

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

[Patrick Massot]

This is only one aspect.

[Patrick Massot]

And dinner is calling

[Reid Barton]

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]

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]

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

[Jalex Stark]

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]

It's broader

[Reid Barton]

Yes, that is certainly an aspect of it.

[Jalex Stark]

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]

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]

is there a guest list?

[Johan Commelin]

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

[Mario Carneiro]

are there any curious mathematicians on the list?

[Johan Commelin]

Not really

[Johan Commelin]

As in, all of them already use Lean

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

you may want to do another advertising run

[Johan Commelin]

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

[Patrick Massot]

Mario Carneiro said:

are there any curious mathematicians on the list?

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

[Johan Commelin]

Oh, that's right

[Patrick Massot]

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]

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]

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

[Johan Commelin]

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]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Bhavik Mehta]

I would argue a strong yes

[Mario Carneiro]

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

[Jalex Stark]

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]

yes

[Jalex Stark]

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

[Mario Carneiro]

exactly

[Reid Barton]

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]

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]

asking for constructiveness at the meta level is irrelevant

[Reid Barton]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Patrick Massot]

You know there is a Type theory stream, right?

[Jalex Stark]

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

[Jalex Stark]

thanks patrick for the diligent moderation

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Jalex Stark]

So should we advertise for "early career researchers"?

[Patrick Massot]

What about "mathematician"?

[Patrick Massot]

Sorry for insisting that some old people still move a bit

[Jalex Stark]

sorry, I only meant to put a lower bound

[Jalex Stark]

"early career researchers and professors"?

[Jalex Stark]

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

[Jalex Stark]

I just want to nail down who they are

[Jalex Stark]

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]

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

[Dima Pasechnik]

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

[Johan Commelin]

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

[Dima Pasechnik]

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]

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