Rogers--Ramanujan identities from the geometry of X^a=Y^b
Yifeng Huang, Kenny Lau, Ken Ono
AI use, as the source states it
“The finite identity and the HJO conjecture have been formalized unconditionally in Lean by AxiomProver.”
Model: AxiomProver, as stated
Named here, or see a mistake? Write to privacy@papex.org.