Trying to test a conjecture

[eengad]

Hi,
Thank you for sharing the code and checkpoint!
I'm trying to use the trained ASTactic model on a conjecture (without a proof), but having trouble getting the conjecture into the agent. Do you have any suggestion?

I couldn't get it into the meta file (either as a conjecture or as a theorem with an aborted empty proof), and couldn't figure out how to hack either coq or extract_proof.py to get it into the json file. Please let me know if you have a suggestion of which file to hack in order to get a conjecture into the json file/agent.

Thanks!

[yangky11]

Hi,

Just an update: Thanks for asking the question. I've been swamped recently and will probably be able to take a look this weekend.

Best,

[eengad]

Thanks! I'm still trying to figure out how to hack it. Any recommendation would be appreciated.

[yangky11]

I don't think the current codebase has direct support for new theorems without proofs. But maybe you can hack it by first adding the same theorem as an axiom, and then proving it using the axiom?

[eengad]

Thanks! That sounds like a good idea, I will try it. I might need to take the axiom off from the json or somewhere else so that ASTactic will not use it for its proof.

[yangky11]

For terms in the global environment, ASTactic only considers those in the same file as the theorem. So it should be sufficient to put the axiom in another file.

[eengad]

Thank you. I will try that.