Comment Comment by Ericson2314 The lede is a bit buried: they're using Lean!This is important for more than Math problems. Making ML models wrestle with proof systems is a good way to avoid bullshit in general.Hopefully more humans write types in Lean and similar systems as a much way of writing prompts. parent Ericson2314 2 years ago
This is important for more than Math problems. Making ML models wrestle with proof systems is a good way to avoid bullshit in general.
Hopefully more humans write types in Lean and similar systems as a much way of writing prompts.