Thomas Hales
Andrew Mellon Professor of Mathematics, University of Pittsburgh
研究领域：Langlands纲领、基本引理，计算机辅助证明（Kepler猜想、蜂巢猜想）、形式证明（Kepler猜想）
A formal proof of the Kepler conjecture
The Kepler Conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space can have density greater than that of the face-centered cubic packing. This talk will describe the history and proof of the conjecture, including early attempts to reduce the problem to a finite calculation, controversy surrounding claimed proofs, the announcement of a proof by Sam Ferguson and me more than 20 years ago, and finally a formal proof of the Kepler conjecture in the HOL Light proof assistant in 2014.
Formalizing mathematics
This talk will describe a broad long-term research program to make formal proofs in mathematics a practical reality. A formal proof is a mathematical proof that has been checked exhaustively by computer, on the basis of the fundamental axioms of mathematics and the primitive inference rules of logic. The field has progressed to the point that it is now possible to give formal proofs of major theorems in mathematics.
Integrating with Logic
In 1995, Kontsevich introduced a new form of integration, call motivic integration. From the start, the development of motivic integration has been guided by model theory, especially quantifier elimination. One particularly useful result has been a far-reaching generalization of the Ax-Kochen-Ersov transfer principle in logic to integration. This talk will give a gentle introduction to motivic integration and will highlight some applications to the Langlands program.
2018 - Hugh Woodin
研究领域：集合论
Ultimate L
The HOD Dichotomy
The Ultimate L Conjecture
2017 - Lou van den Dries
研究领域：代数模型论（application of model theory in algebra）
Model Theory as a Geography of Mathematics
Orders of Infinity and Transseries
Model Theory of Transseries: Results and Open Problems
2016 - William W. Tait
On Skepticism about the Ideal
Cut-Elimination for Subsystems of Classical Second-Order Number Theory: The Predicative Case
Cut-Elimination for Subsystems of Classical Second-Order Number Theory: Cut-Elimination for Π^1_1−CA with the ω-Rule—and Beyond(?)
2015 - Julia Knight
Relationship between computability and definability in familiar kinds of mathematical structures
Computability and complexity of mathematical structures
Comparing classes of countable structures
Computability and complexity of uncountable structures
2014 - Stevo Todorcevic
The Measurability Problem for Boolean Algebras
Chain-conditions of Horn-Tarski
Combinatorial and Set-theoretic Forcing
2013 - Jonathan Pila
研究领域：代数模型论
Rational Points of Definable Sets and Diophantine Problems
Special Points and Ax-Lindemann
The Zilber-Pink Conjecture
2012 - Per Martin-Löf
研究领域：构造主义数学，类型论
Assertion and Inference
Propositions, Truth and Consequence
Tarski’s Metamathematical Reconstruction of the Notions of Truth and Logical Consequence
2011 - Johan van Benthem
研究领域：人工智能中的逻辑
General Lecture: Exploring Logical Dynamics
Logic and Computation: Fine-structure and Invariance
Logic in Games
2010 - Gregory Hjorth
集合论
The Theory of Borel Equivalence Relations in Modern Set Theory
Cardinality and Equivalence Relations
Classification Problems in Mathematics
Borel Equivalence Relations: Dichotomy Theorems and Structure
Download Slides from the lectures
2009 - Anand Pillay
模型论
Compact Space, Definability, and Measures, in Model Theory
The Logic Topology
Lie Groups from Nonstandard Models
Measures and Domination
Download Slides from the lectures
2008 - Yiannis N. Moschovakis
描述集合论，foundation of computer science
Lectures on the Foundations of the Theory of Algorithms
Algorithms and Implementations
English as a Programming Language
The Axiomatic Derivation of Absolute Lower Bounds
Download Slides from the lectures
2007 - Harvey M. Friedman
反推数学
Interpretations of Set Theory in Discrete Mathematics and Informal Thinking
Interpretations, According to Tarski.
Interpreting Set Theory in Discrete Mathematics: Boolean Relation Theory.
Interpreting Set Theory in Informal Thinking: Concept Calculus.
2006 - Solomon Feferman
Truth Unbound
The “Logic” Question
Real Computation
2005 - Zlil Sela
The Elementary Theory of a Free Group
Varieties Over Free Groups
AE Sentences and Quantifier Elimination
2004 - Alexander S. Kechris
New Connections Between Logic, Ramsey Theory, and Topological Dynamics
2003 - Ralph Nelson McKenzie
What is general algebra? (Three lectures)
2002 - Boris Zilber
Dimensions and homogeneity in mathematical structures
The fundamental trichotomy of Geometric Stability Theory, Zariski structures and Diophantine geometry
Pseudo-analytic structures and transcendental Number Theory
2001 - Ronald Jensen
On the Philosophical Foundations of Set Theory
Making cardinals w-Cofinal (Part 1)
Making cardinals w-Cofinal (Part 2)
2000 - Alexander Razborov
Complexity of Proofs and Computations
Interactive and Probabilistically Checkable proofs: A New Paradigm
Algebraic Proof Systems
1999 - Patrick Suppes
Invariance and Meaning
A Physical Model of the Brain’s Computation of Truth
1998 - Angus MacIntyre
Finite Fields and Model Theory
Nonstandard Frobenius Automorphisms
Logic and Intersection Theory
1997 - Menachem Magidor
The Future of Set Theory: Is Gödel’s Program Still Alive?
1996 - Ehud Hrushovski
Interpretations and Geometries
An Application to Diophantine Geometry
1995 - Hilary Putnam
PARADOX LOST? Truth and Hierachies
PARADOX LOST? Sets: Must It Be All or Nothing?
1994 - Michael O. Rabin
Trees, Decidability, and the Logic of Programs
The Truth and Nothing But the Truth: Zero Knowledge Proofs and User Authentication
1993 - Alec James Wilkie
On the Theory of the Real Field with Exponentiation and Other Analytic Functions
1992 - Donald A. Martin
Large Cardinals, Determinacy and the Role of Non-demonstrative
Evidence in Mathematics
1991 - Bjarni Jónsson
Boolean Algebras with Operators
1991 - H. Jerome Keisler
Model-Theoretic Forcing in Analysis
1990 - Willard Van Orman Quine
Reflections on Models and Logical Truth
1989 - Dana Stewart Scott
Wherein Lies the Foundations of Mathematics?
How Far Do We Need to Automate Proofs?
Can We Teach Geometry on the Computer?
网友评论