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