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?