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.
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”.