audience

Stream: Lean for the curious mathematician 2020

[Johan Commelin]

What is our audience?

[Johan Commelin]

Profs? Students? Everyone?

[Jalex Stark]

I think students, where "students" means "people who are in theorem-proving grad school, were in theorem-proving grad school, or could obviously get into theorem-proving grad school if they tried"

[Jalex Stark]

if we're only aiming at theorem-proving profs then getting 10 people seems like a great win

[Jalex Stark]

but we can clearly handle more than that, so we should aim lower

[Jalex Stark]

my "definition" of "student" are people that would be likely to produce interesting content / maybe contribute to mathlib after a few months of practice

[Reid Barton]

I guess maybe the first question is what is the aim.

[Johan Commelin]

Reid Barton said:

I guess maybe the first question is what is the aim.

New topic (-;

[Reid Barton]

I would suggest that a "mathematician" means something like: someone who doesn't know what

$\frac{\Gamma, x : A \vdash e : B} {\Gamma \vdash (\lambda x, e) : A \to B}$

means, but would understand if you explained it to them.

[Jalex Stark]

why not something more like "people who can informally solve all of the problems in first-year maths courses with relative ease"?

[Johan Commelin]

Reid Barton said:

I would suggest that a "mathematician" means something like: someone who doesn't know what

$\frac{\Gamma, x : A \vdash e : B} {\Gamma \vdash (\lambda x, e) : A \to B}$

means, but would understand if you explained it to them.

#!@$!@%#, I'm no longer a mathematician...

[Jalex Stark]

Reid Barton said:

I would suggest that a "mathematician" means something like: someone who doesn't know what

$\frac{\Gamma, x : A \vdash e : B} {\Gamma \vdash (\lambda x, e) : A \to B}$

means, but would understand if you explained it to them.

I guess your definition is broad, it includes many working programmers who essentially do constructive mathematics all day, but they don't use algebra or analysis
Did you mean to catch those people?

[Reid Barton]

Hmm, I didn't really intend to

[Jalex Stark]

Proposal: We're aiming at "mathematicians", where a "mathematician" is someone who could contribute to mathlib without having to learn new math, but may still need to learn Lean

[Jalex Stark]

does that seem right?

[Reid Barton]

I guess I was assuming that the original conference was mostly not aimed at undergrads, if only because for the most part undergrads don't travel to such conferences.

[Jalex Stark]

I went to a conference like this as an undergrad

[Jalex Stark]

where "like this" means "teach the basics of some theorem-proving field, and have some informal research conversations on the side"

[Reid Barton]

So my mental picture of a "mathematician" was more like a grad student/postdoc/faculty.

[Jalex Stark]

The hardest part was getting funding (Caltech has a general fund for undergrad academic travel, but I assume at most schools funding is harder to access), so I think you'd see more undergrads for things like this which are free.
(It kind of sucked to skip a week of class, but not that much? I guess some undergrads care about getting good grades for some reason)

[Reid Barton]

Of course, being online the event now has an entirely different set of constraints so that may not be a reasonable assumption

[Jalex Stark]

also undergrads are looking for things to do because school now _sucks_ compared to school four months ago

[Jalex Stark]

i know plenty who are just taking time off next semester to read books or do research on their own

[Jalex Stark]

(if you have spare funding and want a research assistant, undergrads are "on sale" right now)

[Reid Barton]

I agree it would be great to have some kind of an event targeted at bored undergrads (or high school students). I don't know whether a single event can reasonably target a range that also includes "mathematicians"; maybe it can. At a minimum, I think it needs to be advertised differently.

[Jalex Stark]

right

[Jalex Stark]

my only point is that any reasonable definition of "mathematician" includes some people who are still undergrads

[Jalex Stark]

like, it should include all people who write serious papers that prove new theorems and post them to arxiv, right?

[Jalex Stark]

i think i've seen the phrase "grad students and advanced undergrads" used for things like this before

[Mario Carneiro]

There aren't many undergrads in that category, and those that are know what they are getting into

[Jalex Stark]

yeah, I agree you don't need special advertising for them

[Jalex Stark]

I brought this up only for helping define the set of people we're after

[Jalex Stark]

and to point out that "has enrolled in a PhD program" is not true for all of the people we're after

[Reid Barton]

Basically, I'm imagining that it is centered somewhere around "postdocs", and has a small enough radius to be manageable, whatever that means.

[Reid Barton]

Of course not all, but maybe like 80%.

[Reid Barton]

Maybe 80% is too high, I don't know.

[Jalex Stark]

i'm imagining the center is more like second-year grad students

[Jalex Stark]

because postdocs need to write papers that prove new theorems to get jobs

[Jalex Stark]

at least this is the case in TCS (=theoretical computer science, the theorem-proving community i'm most familiar with, people who prove things about complexity classes and quantum computers and fourier analysis on the boolean cube)