2026.02.19 15:33:49 (Mastodon 116098022047921483, Twitter 2024507732582420965) from Daniel J. Bernstein:
People with enough confidence in proof-checking software have been happily letting LLMs write proofs. For example, https://github.com/jrh13/hol-light/commit/0a5e935c976d1ff780906c23b8f82939189844e5 has an LLM translation of some proofs from math textbooks into HOL Light, a proof checker that has survived particularly intense audits.