Big Proofs and Formal Abstracts
Người báo cáo: Giáo sư Thomas Hales

Thời gian: 1h30, Thứ 3 ngày 26/12/2017
Địa điểm: Phòng 611-612 Tầng 6 Nhà A6
Tóm tắt: Proof assistants have been used to verify complicated proofs such as the Kepler conjecture in discrete geometry and theorems in group theory. Can formal proof technology help us to understand the statements of complicated conjectures such as Millennium (million-dollar) problems of the Clay Institute, the Langlands program, or the Kelvin problem for optimal partitions of space?

Trở lại