2025.06.18 08:08:44 (Mastodon 114703343600662470, Twitter 1935248312187421027) from Daniel J. Bernstein:
You're writing a paper with a proof checked by HOL Light. Do you copy the theorem statement in HOL Light format into the paper? Manually translate it to normal format, risking error? My new HOLTrace package automatically translates the theorem statement: https://holtrace.cr.yp.to