Hi Mario, > I am interested in formalizing results about the game of Go as my next > project. I have have a repository of computer-verified proofs here: > https://puszcza.gnu.org.ua/projects/hol-proofs/
I am very interested in such a project; please let me know about your progress! I don't know about your plans, but the foremost thing I want to do is to determine the theoretical komi for small rectangular boards in a proof assistant; in particular, to reproduce most and hopefully all results in the two papers "Solving Go on Small Boards" and "Solving Go for Small Rectangular Boards". I don't expect tree search to be as efficient in a proof assistant, but more powerful arguments (or "proof tactics") may compensate for that. To make things more efficient, it may be desirable to implement bitboard and hashtable in the proof assistant. I have been wondering what proof assistant I should use. Coq seems to be a suitable choice, since people have been using it for retrograde analysis in chess, and it's also what the machine learning environment GamePad uses. ( https://arxiv.org/abs/1806.00608) But personally I am familiar with neither Coq nor HOL to judge which will be more efficient for proving facts about Go. 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. 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 terms of tsumego difficulty, 6x6 optimal solution is about amateur 6d, and 7x7 is much harder than Hatsuyōron problems. The most important reason is that a usual tsumego has only one solution, which is not the case for an empty small board (and we have no idea how many solutions there are)." Compared to the 7x7 article by J. Davies, it also explains why some variations do not work. There has been a debate here 10 years ago about 6x6 komi; now people seem to have settled that it's 4, but a computer proof is still lacking. If anyone has trained 6x6 networks with komi's 3.5/4.5 which have nearly 100%/0% initial winrate respectively, that would be very helpful for the move ordering in the tree search stage (and the winrate would help determine when to apply other proof tactics), but these are easy to train nowadays anyway (using Leela Zero or Minigo or whatever). Best, Junyan
_______________________________________________ Computer-go mailing list Computer-go@computer-go.org http://computer-go.org/mailman/listinfo/computer-go
