<p><span class="h-card" translate="no"><a href="https://mastodon.social/@whitequark" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>whitequark</span></a></span> i know I've seen terence tao throw around the idea of asking LLMs to generate machine proofs in Lean or whatever, since doing the actual formalization is often annoying and the result is verifiable</p>