-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
experiment: Proof search function from llemma_formal2formal #6
base: brando
Are you sure you want to change the base?
Conversation
NeurIPS has extended the deadline for adding authors. You can join the author list if we get this experiment going. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
On proof_search.py:287
, the first goal of a given state is handled. When do you handle other goals?
I am not sure if this is exactly how the GoalState variable works with pantograph and Lean 4 in general, but I was under the impression that when a goal is complete, it is removed from the list of goals in the given GoalState variable. Then, with multi-goal states, it would go through the goals individually until the entire state is solved. Then, just focusing the on the first goal of a given state would be sufficient in proving the entire theorem. |
No that is not how it works. I intentionally designed it so that each goal has to be solved individually, so if a state has goal 0,1,2, there would be calls to |
Just to confirm, when a goal is proved, it is removed from the GoalState goals array right? Would the index of the remaining goals then be shifted up? I guess one confusing thing is that the is_solved function for the GoalState returns whether the goals array is empty or not, so it seems like the goals are deleted as they are proved. |
every time you execute a tactic on a goal state, the state itself doesn't change, but it produces a new state which can have 0 or more goals. if it has 0 goals and isn't coupled (i think i didn't implement this part), the state is solved. |
Take a look at this: #10 |
Were you able to get this to work? If you have trouble with the proof search loop, I'm about to add a new feature where Pantograph will automatically give the next goal to the user to solve. #11 |
I modified the |
Hello! I implemented the proof search function from Welleck's llemma_formal2formal project and tested it on some base theorems (the ones used in the pantograph/server.py tests).
The main additions are listed below:
Thank you!