Regardless of whether the target result(s) are ultimately correct, isn't it almost guaranteed that supporting infrastructure for surreals-in-lean is a real contribution? Is it a goal to make those polished/reusable, or more like throw-away harness, and just a stepping stone to the proof?
I'm a little tired from the project so not eager to jump back into it right away. But yes, I'd love for useful pieces to make their way into https://github.com/vihdzp/combinatorial-games. Violeta, who maintains CG, expressed interest in ultimately integrating the proof in some shape into the repo, but I think more work needs to be done to understand what makes it work.
I've confirmed with the mathematicians working in that field that this is a new result.
Regardless of whether the target result(s) are ultimately correct, isn't it almost guaranteed that supporting infrastructure for surreals-in-lean is a real contribution? Is it a goal to make those polished/reusable, or more like throw-away harness, and just a stepping stone to the proof?
I'm a little tired from the project so not eager to jump back into it right away. But yes, I'd love for useful pieces to make their way into https://github.com/vihdzp/combinatorial-games. Violeta, who maintains CG, expressed interest in ultimately integrating the proof in some shape into the repo, but I think more work needs to be done to understand what makes it work.