Open post seewoo5 @seewoo5@mathstodon.xyz · 7mo ago Replying to @MoritzFirsching@mathstodon.xyz <p><a href="https://mathoverflow.net/questions/486451/reference-request-right-local-semirings/508783#508783" target="_blank" rel="nofollow noopener" translate="no"><span class="invisible">https://</span><span class="ellipsis">mathoverflow.net/questions/486</span><span class="invisible">451/reference-request-right-local-semirings/508783#508783</span></a></p><p>I'm quite happy how this worked:</p><p>(1) Junyan Xu comes up with a question<br />(2) formalises it and puts it into <a href="https://github.com/google-deepmind/formal-conjectures" target="_blank" rel="nofollow noopener" translate="no"><span class="invisible">https://</span><span class="ellipsis">github.com/google-deepmind/for</span><span class="invisible">mal-conjectures</span></a><br />(3) it gets solved!</p><p>This is working as intended... </p><p>When you have a mathematical question you are interested in, and it is not too hard to formalise, consider adding it to Formal Conejctures!</p> @MoritzFirsching Interesting! How did you come up with (informal) answer? Probably some AI-assisted or just humans?
Open post seewoo5 @seewoo5@mathstodon.xyz · 7mo ago Replying to @MoritzFirsching@mathstodon.xyz @seewoo5 The autogenerated formal answer was quite readable and even had code comments @MoritzFirsching That’s nice!