I recommend refraining from making (and especially from posting) any conclusions until then.

Strongly reminds me of "no true scotsman."

If you have an access to a good model, try that simple problem of blocked clause decomposition and please get back to us.

Please preface your future posts on the topic with “I’ve never tried any decent models, so I don’t know what I’m talking about”.

I, actually, asked my friend to ask whatever LLM he paid for to perform this experiment. I think he uses latest or previous GPT. At least he is paying for it which I cannot do and won't do in foreseeable future.

Just like I said above, not only LLM failed to properly implement the algorithm, it failed to provide even remotely correct types for clauses and blocked clauses.

What happened next amused me like nothing else related to AI.

The exchange that followed incorrect initial attempt, GPT clearly tried to persuade my friend to implement the correct version for it, constantly providing him with partially (and stupidly) incorrect code.

This is exactly what MathCraft [1] does.

[1] https://en.wikipedia.org/wiki/Cyc#MathCraft

And this behavior is clealy counterproductive. This is not what one might expect from anything that is advertized as a good assisting measure. I can use ghci, vim and actual paper with much greater effect.

Essentially why the current batch of top-tier LLMs are trained on a pile of text amounting to “the internet”, containing every haskell q&a on stackoverflow, every sat implementation on github, and every explaination of those terms on wikipedia. It might seem unreasonable without the sense of scale and expense of building these things; but yes, it has those input data in its training set.

For LLM to implement BCD in Haskell it needs to be able to translate between Haskell and C++ and it is well beyond trivial.