2024.11.22 21:22:14 (Mastodon 113528703178556352, Twitter 1860071342466641939) from Daniel J. Bernstein:
For the people who've asked whether my next computer-checked-proof projects would be in HOL Light or in Lean after I did both for https://cr.yp.to/papers.html#goppadecoding (see https://cr.yp.to/papers.html#pwccp for notes on procedures): https://cr.yp.to/2024/transcendence-pi-20241122.ml is a proof of transcendence of pi in HOL Light.