Talagrand Problems

Stream: Formal conjectures

[Franz Huschenbeth]

List of Problems with Prizes from Talagrand:
https://michel.talagrand.net/prizes/

[Moritz Firsching]

Seems like potentially good problem, some of them somewhat difficult on top of current mathlib.

Seeing these problems with prizes recently, perhaps we could extend our category attribute

@[category research open, AMS 11, 🤑 "$100"]
theorem foo ...

[Franz Huschenbeth]

Moritz Firsching said:

Seems like potentially good problem, some of them somewhat difficult on top of current mathlib.

Seeing these problems with prizes recently, perhaps we could extend our category attribute

@[category research open, AMS 11, 🤑 "$100"]
theorem foo ...

AlpahProof will gladly take the prize money to buy himself more compute :laughing:

[Franz Huschenbeth]

Raised all the 4 problems each worth 1k$. His Convexity Problem is the easiest to formalize.