@pozander @lu_sichu it is a bit confusing. afaiui what they're saying is that output a) wasn't guided by an external judge / verifier (noam confirmed the solve didn't use lean), though it might've been detected by one, and b) the final proof was rewritten for simplicity w/ human assistance (see img) https://t.co/rybdPgRXYC
same thread: 2057198687307362642 2057209351564153130 2057211346505396326 2057211930625077327 2057224392388829529 2057225314070409691 2057227285200249130 2057227858146439434 2057276594608349565 2057282565816668391 2057282690513027344 2057282844247089186 2057293031745970240 2057298916023079034 2057304902985187384 2057338667639980183 2057342482778927352 2057346427194597454 2057346768929776062 2057349505562104289
Reproduced against link rot, credited and linked to its original. Yours and you’d rather it weren’t here? Open an issue.