Yutaka Ng

Suggestion: declare that this repository is no longer maintained.

1

Dear @DyeKuu , I guess nobody has the admin right to handle pull requests to this repository and the development of miniF2F is continuing at [the corresponding repository at Facebook...

- Domain-specific optimisations? - [ ] Avoid template-based conjecturing when no user-defined types appear in the proof goal. - [ ] More tactics for math problems. - [ ] math_olympic...

This would be useful for debugging as well.

Abduction: another way to detect bad applications of induction

1

1. We apply the `induct` tactic. 2. We get a step case whose shape looks like `induction_hypothesis ==> conclusion`. 3. Take `conclusion` from this step case. 4. Apply `clarsimp to...

UR: design decisions for the first prototype.

4

- bottom-up conjecturing or goal-oriented conjecturing? Both: bidirectional conjecturing. - structural proofs or backwards proofs? - Both: structural proofs for bottom-up conjecturing and backwards proofs for goal-oriented conjecturing. - Note...

We should be able to reason about types of HOL to efficiently produce types.

UR: assertions on the log.

1

For example, if two alpha-equivalent nodes appear twice in the same path, probably something has gone wrong. We can improve the accuracy of pruning by developing assertions on the log/path.

Can we get rid of chained state from `seed_of_or2and_edge`?

1

Can we get rid of chained states from `seed_of_or2and_edge`? Instead of passing a chained state that we obtain after applying certain proof methods, I would like to reconstruct such proof...