Kourovka

Stream: Formal conjectures

[Ralf Stephan]

I'm done with making issues out of Kourovka ed. 1. Now, since I'm not a group theorist or topologist I took Gemini's summaries and just edited them. The statements in Kourovka that were already formalizable should be fine. However, the issues I created where there was only a sentence in Kourovka like "Describe XY", I asked Gemini for formalizable questions, so these are essentially Gemini's questions/conjectures and possibly only stated here. You can recognize these issues: the title shows a topic after the number.

Please give feedback: is this approach acceptable? I guess hallucinations are less probable because long-standing problems have a lot of literature.

[Moritz Firsching]

Thanks! I think it is great to have open Issues for all problems in Kourovka, so ed.1 is a great start.
I think the approach using Gemini (or whatever) to get some info on them and what is needed in mathlib as long as it is reviewed somewhat carefully. The issue-creation has multiple purposes: point people to interesting open conjectures, and make it somewhat easy to estimate how difficult it would be to work on. Also it is good to avoid duplicate work. So most of this is also works when the issue creation is not absolutely perfect.

[Moritz Firsching]

One question about Kourovka: they update solutions, right? So if a problem if solved it will be marked in the next edition?

[Ralf Stephan]

Solved problems are removed from the main section and moved to the archive appendix in the same publication.