2 ms·
Perhaps one thing you should devote effort to is ensuring this has not already been proved in the literature.
by j2kun 2mo ago
Perhaps one thing you should devote effort to is ensuring this has not already been proved in the literature.
- danabramov 2mo agoI've confirmed with the mathematicians working in that field that this is a new result.
- ianjbutler 2mo agoRegardless 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?
- danabramov 2mo agoI'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 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.