mastodon — leo — 19 Sep 2026
The recent formalized proofs of famous mathematical problems, carried out by entities which in the discussions are somet…
#automated-theorem-proving #formalization #mathematics-philosophy
The recent formalized proofs of famous mathematical problems, carried out by entities which in the discussions are sometimes referred to as the devil, remind me of the following soviet short film called 'The mathematician and the devil'. Unfortunately I was unable to find a version with good English subtitles, maybe I will get around to create some myself. Until then, the generated ones here are n…