Hello Junyan (I assume that is your given name; apologies if I am wrong). Unfortunately I do not have time to read in detail all your links, but I took a glance at all of them.
> I have been wondering what proof assistant I should use There are many proof assistants; my only real experience is with HOL4 and I can recommend it. I do not recommend Coq because its logic is very complex and appears to be nowhere described in full detail. In my opinion, formalizing something in a proof assistant whose logical framework is uncertain defeats the purpose of formalizing the theory in the first place. Originally I started learning Coq but I switched to HOL4 after became aware of this shortcoming. The logic of HOL4 is very simple (subjectively, simpler than ZFC) and a description in the natural language customarily used for mathematics is found in the HOL4 manual. The base logic of HOL4 is proven consistent relative to ZFC. Normally one works by adding definitions that preserve soundness (assured by the logical kernel). If needed, axioms can be added easily, to have a stronger theory, losing the soundness guarantee. HOL4 is basically an implementation of the formalization of higher order logic as a typed lambda calculus proposed by Church in 1940. HOL4 is written as just a library in the Standard ML programming language. Thus it can be extended easily with derived inference rules and the logical kernel verifies the primitive inference steps, thereby there is no risk of introducing unsoundness with new proof tools. One can also formalize and _run_ functional programs within the HOL4 logic. There is an extensible library “computeLib” that returns a theorem equating the original expression to its evaluated form according to the transformation rules defined by the user; the resulting theorem is like any other in that it is created using the primitive inference rules and the same soundness guarantees apply. > It's probably hopeless to determine the best play for an arbitrary > initial position, but starting from the empty board, there should be > relatively simple forced lines towards the optimal score under different > rulesets: at least many human individuals have pruned the game tree > enough that they are convinced of the alleged optimal solutions for 6x6 > and 7x7, and computers can be more exhaustive and quicker through > automation. That's why I believe producing formally verified proofs is a > feasible task with the advent of deep learning. Formalizing results for small boards is an interesting project. In HOL4 one would write a decision procedure for Go that generates a proof verified by the kernel, just as we already have for Presburger arithmetic, boolean formulas and some more. I suspect the key to fast decision procedures for Go is using the advances of SAT solvers: clause learning, restarts, and some heuristics. Intuitively, I doubt that the computer learning “““advances””” applying ANN to Go will be of any use in automated theorem proving. The field of computer learning, and the computers used thereby have been getting dumber since it started. Around 40 years ago computer learning was about giving _provably_ correct answers to extremely hard problems. The hot topics were automated theorem proving and constraint satisfaction solvers and decision procedures. Great theoretical and practical advances were made. Now “computer learning”, “deep learning”, etc. is just applying heuristics at vaguely defined problems to get approximate answers. They use the dumbest hardware that I have seen: vector computers (“““GPGPU”””) that can only do brute number crunching with small floats (and they are often not even IEEE 754 compliant!!!). What a shame. > For interested people, this 2015 article is the most comprehensive > analysis of 7x7 Go (by Li Zhe 6p) I've seen: > https://m.newsmth.net/article/Weiqi/615932 In my browser it shows as a blank page. I can not promise any immediate result or cooperation, because I am still working with my formalization of Gregorian calendars algorithms in HOL4, but I am interested in writing a decision procedure for Go coupled with the HOL4 proof assistant. Regards.
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Computer-go mailing list Computer-go@computer-go.org http://computer-go.org/mailman/listinfo/computer-go
