A Milestone in Formalization: The Sphere Packing Problem in Dimension 8
Created by
- Haebom
Category
Empty
μ μ
Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska
π‘ κ°μ
λ³Έ λ
Όλ¬Έμ 8μ°¨μ ꡬ μκΈ° λ¬Έμ μ νκΈ°μ μΈ ν΄κ²°μ νμννλ κ³Όμ μ λν λ΄μ©μ λ€λ£Ήλλ€. Viazovskaμ 2016λ
ν΄κ²°μ±
μ Lean μ 리 μ¦λͺ
κΈ°μμ 곡μμ μΌλ‘ κ²μ¦νμΌλ©°, νΉν Math, Inc.μ μλ νμν λͺ¨λΈ 'Gauss'κ° μ΅μ’
κ²μ¦ λ¨κ³λ₯Ό λ΄λΉνμ΅λλ€. μ΄λ μΈκ°κ³Ό Gauss κ°μ λ
νΉν νμ
μ ν΅ν΄ λ¬μ±λ μ€μν μ±κ³Όμ
λλ€.
π μμ¬μ λ° νκ³
β’
λκ·λͺ¨ μν μ 리λ₯Ό νμμ μΌλ‘ κ²μ¦νλ λ° μλνλ AI λͺ¨λΈμ΄ μΈκ° μ λ¬Έκ°μ νλ ₯νμ¬ μ€μν μν μ ν μ μμμ 보μ¬μ£Όμμ΅λλ€.
β’
μνμ λμ λ₯Ό ν΄κ²°νλ κ³Όμ μμ AIμ νμν λ₯λ ₯μ΄ μ
μ¦λμμΌλ©°, ν₯ν μν μ°κ΅¬μ ν¨μ¨μ±μ λμΌ μ μ¬λ ₯μ μμ¬ν©λλ€.
β’
μμ§ νμνλμ§ μμ κ΄λ ¨ μνμ μ¬μ€λ€μ΄ λ¨μ μμΌλ©°, μ΄λ ν₯ν μ°κ΅¬ κ³Όμ λ‘ λ¨μμμ΅λλ€.
