Demand for handwritten solutions?

Stream: IMO-grand-challenge

[Clayton Knittel]

Hi all, new to lean here. I recently wrote a solution to IMO 2023 P1 and wanted to know what the demand for handwritten proofs are. I see a lot of talk about AI written proofs here, but not much about finding proofs by hand. I have been having fun writing them and am working on 2018 P2 now, so I'm curious if this work will lead to anything meaningful.

[Kevin Buzzard]

Proofs for all past IMO problems are up on the internet and will have been seen by all the modern language models. There might be an interest in proofs which are genuinely different to those documented in places such as AOPS but conversely it might be quite tough to find a new proof which isn't already up there in some form

[Kim Morrison]

Proofs of IMO problems are accepted in the Archive/IMO/ directory of Mathlib, although we'd prefer that they are "exemplary" solutions (e.g. making proper use of mathlib rather than proving anything useful locally, and making good use of tactics, and good proof style).

[Jason Rute]

Also, @David Renshaw has a repository of such proofs at https://github.com/dwrensha/compfiles/tree/main/Compfiles

[Jason Rute]

So sorry. Your link was to a compfiles PR.

[Clayton Knittel]

I did rely on some general reasoning about factorizations in my proof that took up a lot of space. The biggest offender was the fact that if n is not a prime power, then let p = n.minFac, q = (ordCompl[p] n).minFac, we have p < q and p and q are both primes. Is it reasonable for proofs like this to require a lot of code? In my limited experience, I have needed to show "obvious" facts like this using a lot of code, failing to find anything that gives me exactly what I need in mathlib

[Kim Morrison]

Reusable statements like this should be PR'd to Mathlib. This is part of the requirement for IMO problems to go in Archive/.