### Recent Comments

Gil Kalai on To Cheer You Up in Difficult T… Gil Kalai on To Cheer You Up in Difficult T… Alexander Barvinok on To Cheer You Up in Difficult T… Kevin on To Cheer You Up in Difficult T… Gil Kalai on To Cheer You Up in Difficult T… Arseniy on To Cheer You Up in Difficult T… Alexander Barvinok on To Cheer You Up in Difficult T… uniform on To Cheer You Up in Difficult T… Arseniy on To Cheer You Up in Difficult T… normanstresskopf on To Cheer You Up in Difficult T… To Cheer You Up in D… on Beyond the g-conjecture… To Cheer You Up in D… on Euler’s Formula, Fibonac… -
### Recent Posts

- To Cheer You Up in Difficult Times 31: Federico Ardila’s Four Axioms for Cultivating Diversity
- Dream a Little Dream: Quantum Computer Poetry for the Skeptics (Part I, mainly 2019)
- To Cheer you up in difficult times 30: Irit Dinur, Shai Evra, Ron Livne, Alex Lubotzky, and Shahar Mozes Constructed Locally Testable Codes with Constant Rate, Distance, and Locality
- To cheer you up in difficult times 29: Free will, predictability and quantum computers
- Alef’s corner: Mathematical research
- Let me tell you about three of my recent papers
- Mathematical news to cheer you up
- To Cheer You Up in Difficult Times 28: Math On the Beach (Alef’s Corner)
- To cheer you up in difficult times 27: A major recent “Lean” proof verification

### Top Posts & Pages

- To Cheer You Up in Difficult Times 31: Federico Ardila's Four Axioms for Cultivating Diversity
- The Intermediate Value Theorem Applied to Football
- Extremal Combinatorics III: Some Basic Theorems
- Amazing: Karim Adiprasito proved the g-conjecture for spheres!
- Updates and plans III.
- Answer: Lord Kelvin, The Age of the Earth, and the Age of the Sun
- An interview with Noga Alon
- TYI 30: Expected number of Dice throws
- To Cheer you up in difficult times 30: Irit Dinur, Shai Evra, Ron Livne, Alex Lubotzky, and Shahar Mozes Constructed Locally Testable Codes with Constant Rate, Distance, and Locality

### RSS

# Monthly Archives: June 2021

## To cheer you up in difficult times 27: A major recent “Lean” proof verification

“Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover.” (See Lean’s homepage and see here for an introduction to lean.) Kevin Buzzard’s blog … Continue reading

Posted in Algebra, Updates, What is Mathematics
Tagged Kevin Buzzard, Lean, Peter Scholze
4 Comments

## To cheer you up in difficult times 26: Two real-life lectures yesterday at the Technion

After 16 months without lecturing to an audience in my same location, I gave yesterday two lectures at the Technion in front of a live audience (and some additional audience in remote locations). The main lecture was in COMSOC 2021, … Continue reading

Posted in Combinatorics, Convex polytopes, Economics, Games, Rationality
Tagged COMSOC 2021
Leave a comment