DSL for theorem proving?

Stream: Machine Learning for Theorem Proving

[(deleted)]

https://gist.github.com/huynhtrankhanh/b9b5f0bca44f3d1aa6bd7148ece7f710

I'm trying to make a DSL for theorem proving in a limited domain. However, DeepSeek R1, Gemini 2.5 Pro and Claude Opus are all unable to generate a correct proof. What should I do here? Can I tweak the prompt?

[(deleted)]

I would like to apologize in advance for the broken Chinese.

[(deleted)]

Do I need Gemini Deep Think? I feel I might need it. It is my only hope. My language is so clearly specified.

[(deleted)]

UPDATE: the answer is indeed just use a better reasoning model, and let it think for around 11min.

[(deleted)]

The community could steal a page from this. If you have a massive number of theorems to prove, it's possible to make a DSL and make a strong reasoning model prove theorems with the DSL.

[GasStationManager]

Looks interesting, thanks for sharing!

I'm trying to understand what is the advantage of this DSL, over doing the proof in Lean. Is it more powerful tactics? Even if that's the case, could have defined those tactics in Lean. Perhaps it is because this DSL has a very limited set of choices (compared to Lean), so if the model tries to do a (more exhaustive) search for proof there is better chance of succeeding?

[(deleted)]

Yes, the limited set of choices is the very point. So the model doesn't have to waste time doing RAG and risk degrading performance.

[GasStationManager]

Huỳnh Trần Khanh said:

UPDATE: the answer is indeed just use a better reasoning model, and let it think for around 11min.

Does the model run the code during that 11 minute think, or is it purely chain-of-thought?

[(deleted)]

It is purely chain of thought. I'm working on an MCP server to validate the code so that less expensive models can be used.

[(deleted)]

https://github.com/huynhtrankhanh/ComplexNumberProofAssistant/

[(deleted)]

Enjoy the MCP server!

[(deleted)]

Moving forward this represents a promising model for automated theorem proving.

[(deleted)]

We should make more MCP servers for various domains of mathematics to harness the reasoning power of LLMs.

[(deleted)]

Oh sorry... I still have to clean up the LLM generated mess. The fight is not over, and AI hasn't replaced programmers yet.

[GasStationManager]

Cool! From what I understand, this produces a proof in the DSL; would it be possible to automatically translate it into a Lean proof script?

[(deleted)]

Very simple, I just need to modify the pretty printing function... But I have to get the server to work first. It still doesn't run properly.