I'd like to have a look through the lean4 proof from openAI's recent paper: Modularity of elliptic curves over imaginary quadratic fields <https://github.com/openai/math/blob/main/preprints/Modularity-of-elliptic-curves-over-imaginary-quadratic-fields-October-4-2026/paper.pdf>. I've had a look round the openai github but i can't find the lean4 proof. did openai publish the lean4 code? if so, could you link it to me?
No idea of that particular case, but OpenAI only published like half of the proof with a Lean program. The other half is only in English. Most of the only-English proof are probably correct, but they already retracted 3 and fixed 10, so expect a few more surprises.