Lean for the ?_ Mathematician

Stream: general

[Alex Kontorovich]

There will soon be an announcement about an upcoming workshop that @Heather Macbeth @Antoine Chambert-Loir and I are organizing, hosted by the Simons Foundation in NYC (June 16-27), of the "Lean for the Curious Mathematician" flavor. Question:

Is it time to move on from "Curious" in the name, which can have a less serious connotation, to something like "Research"?

The shift from "Curious" to "Research" would reflect an evolution in Lean's position within mathematics. While "Curious" suggests an exploratory, opt-in approach that made sense when formal verification was more niche, "Research" positions Lean as a mainstream research tool that working mathematicians might naturally want to incorporate into their practice. Moreover:

1. It avoids any potential perception that these workshops are introductory or recreational rather than professionally relevant
2. It aligns with how other professional mathematical tools and workshops are typically branded (e.g., "Research Symposium on...")
3. It might help with grant applications and institutional support by clearly signaling its relevance to research activities

I realize there's a long history of the "Curious" version, so those of us already doing this kind of work are accustomed to it, but I think to reach the broader base of researchers, it might be time to label it as such? What do people think?

[Johan Commelin]

Good suggestion! My gut reaction is: we can have both, depending on the type of workshop. The more introductory tutorial-like workshops can continue the "Curious" tradition. But why not add "Research" versions as well?

[Alex Kontorovich]

Oh yes, thanks! This was not to say that others shouldn't continue to call their workshops "Curious" if they so choose. But if we were to consider calling ours "Research", would that go against the grain of the community?

[Jeremy Avigad]

I like the idea of using "research" in the title, for the reasons you mention.

[Notification Bot]

Antoine Chambert-Loir has marked this topic as resolved.

[Kevin Buzzard]

So that's settled then :-)

[Notification Bot]

Kevin Buzzard has marked this topic as unresolved.

[Siddhartha Gadgil]

Not that I have anything against "research", but I always understood "curious" here to mean curious about Lean (and actually a mathematician).

Also "Lean for the working mathematician" will follow a tradition (I am sure this was considered, but just mentioning for completeness).

[Patrick Massot]

If you choose to use “Lean for the research mathematician” then you should be aware that the Lean for the curious mathematician always attracted also people interested in Lean for teaching and they may feel less welcome with your new title.

[Matthew Ballard]

I like the original suggestion: "Lean for the ?_ Mathematician" ;)

[Ruben Van de Velde]

Lean for the sorry mathematician? No, I don't think that works

[Edward van de Meent]

something something don't know how to synthesize placeholder

[Jeremy Avigad]

Sorry to be boring about it, but there's always "Lean for Mathematicians" ...

[Edward van de Meent]

"Lean for the [your predicate here] Mathematician"

[Jireh Loreaux]

Jeremy Avigad said:

Sorry to be boring about it, but there's always "Lean for Mathematicians" ...

In fact, we have already advertized it under this name, just not in English: Lean pour mathématiciens

[Etienne Marion]

The explanation being that French mathematicians are all curious from what was said there :wink: