{"ID":2869440,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.15116","arxiv_id":"2509.15116","title":"The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction","abstract":"We formalize the multi-graded Proj construction in Lean4, illustrating mechanized mathematics and formalization.","short_abstract":"We formalize the multi-graded Proj construction in Lean4, illustrating mechanized mathematics and formalization.","url_abs":"https://arxiv.org/abs/2509.15116","url_pdf":"https://arxiv.org/pdf/2509.15116v1","authors":"[\"Arnaud Mayeux\",\"Jujian Zhang\"]","published":"2025-09-18T16:19:41Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.AI\",\"math.AG\"]","methods":"[]","has_code":false}