Questions from an intrigued undergraduate student

[lnishan]

Hello, I've quickly glanced through the paper.
I have some questions:

1. Are there any missing files?
   From Line 77, there seems to be files used for verification, but they don't seem to be anywhere in this repo.
2. What prompted you to employ genetic programming approaches?
   In this paper you've mentioned AlphaGo and Monte Carlo Tree Search, but the concepts are fundamentally different. Hence, I'm wondering why you used genetic programming approaches in the first place.
3. What would be some limitations?
   In the 10 theorems you've shown, both sides of the equations are known. What about proofs with undetermined results (ie. right-hand side)?
4. Future directions?
   A proof is usually derived based on known facts (or theorems). You've mentioned a database of theorems, but it does not seem to be accounted for in the algorithms present. I'm interested in how this can be handled. Are there any ideas in mind?

[lnishan]

I guess it's odd from a student's perspective to ask these questions.

Closed issue :) Nvm

[ypchen-tw]

Hi, there! Questions are welcome, and the status, e.g., student or not, is irrelevant.

Regarding your questions, I can provide you what I know and remember:

1. That part of code is currently not (actually) used, and the *_verify.v files are generated along the process. So, the short answer is that there is no missing file.
2. The motivation is described in our paper available on arxiv. Since genetic programming is a technique to generate programs and programs can be considered as proofs, using genetic programming to search for proofs then seems intuitive. While MCTS may be quite different from GP, it is still a kind of search technique. As we described in the paper, significant amount of effort may be needed if MCTS is to be adopted to search for proofs.
3. I am not sure what you meant. A mathematical/logical statement must be well defined, and proving it is then possible. If you would like to "determine" certain undetermined results, that would be more "calculation" or "computation" type of work, instead of the "proof" type of work we considered in this study.
4. I am not sure what you meant by "a proof is usually derived based on known facts (or theorems)." Generally, we apply logical inference rules on axioms (and/or theorems) to (construct a proof to) prove a logical sentence, and then the sentence is called a theorem. The database of theorems used in this study currently consist of those Coq built-in axioms and theorems and also Definitions.v in the repository. Our current implementation does not directly interface with the database of axioms/theorems.

[lnishan]

Thanks for the reply, professor! :)

Sorry for the late reply. I've been quite sick lately.

=> 3. Yes it seems I had some terms mixed up. I was thinking more like formulas. But still, can there be existing theorems left to be explored? Maybe let's say if we have Theorem A, B, C and we can actually get Theorem D (maybe not known previously) for free? These days I heard interdisciplinary researches are quite popular, so maybe having a database of theorems from multiple disciplines would speedup this process? => 4. I see, but would be interesting to see how the research goes! Very intriguing research topic indeed!

Sorry about my ignorance. I think I still have a lot to learn :D

Oh and, Good luck on the paper submission!

[ypchen-tw]

Hm... what do you mean by "for free?" Aren't all theorems proven based on axioms and/or previously proven theorems? Some theorems may be proven with fewer steps of inference and others more steps. It depends on how you think of "free."

Moreover, "a database of theorems from multiple disciplines"... are these "multiple disciplines" within mathematics or not? Currently, we are considering "theorems" as in the sense of logical systems and/or mathematics.