Monthly Archives: June 2021

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

Posted on June 30, 2021 by Gil Kalai

“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 , , | 5 Comments

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

Posted on June 9, 2021 by Gil Kalai

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 | Leave a comment