@zwarich @tmyklebu The main downside compared to something like Coq or Lean is that failures are a lot more non-informative unless you've already subdivided your proof obligation into small enough pieces that the mere failure to prove a piece gives a strong indication of what went wrong/what is missing. Dunno how much of that could be improved given the relatively black box nature of ATPs.
=> More informations about this toot | View the thread | More toots from pervognsen@mastodon.social
=> View zwarich@hachyderm.io profile | View tmyklebu@mastodon.gamedev.place profile
text/geminiThis content has been proxied by September (3851b).