Mellon Professor, University of Pittsburgh Thackeray 416 412-624-8375 Email: MYLASTNAME AT PITT DOT EDU Encryption Works! Fight surveillance!- Chat with OTR messaging; browse with Tor and https; disable javascript and cookies; encrypt your cloud storage (dropbox, etc.); boycott products (gmail, skype, etc.) that are based on privacy policies rather than end-to-end encryption; shutter FB; become a cryptographer and design anti-surveillance tools; smash your tracking devices (cell phones); voice your rights; march on Washington.
Blog- Pitt Intellectual Property (Jan 2016)
- the NSA back door to NIST (published in the Notices of the AMS).
- Formalizing NIST standards (Nov 2013)
- 27 formal proof projects
Teaching - Algebraic Geometry (Math 2810, Spring 2016)
- Introduction to Mathematical Cryptography (Math 1025, Spring 2016)
Pitt Algebra, Combinatorics, and Geometry Research Group- Research group projects
- Pitt's ACOG seminar
- Graduate students, past and present
- Endoscopic transfer of orbital integrals in large residual characteristic (with J. Gordon)
- The Formal Proof of the Kepler Conjecture (with many coauthors, including Hoang Le Truong and A. Solovyev). The project is officially complete.
- Bourbaki report on Developments in Formal Proofs (pdf) (youtube)
- (with A. Solovyev) Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations, 2012
- A Proof of Fejes Toth's Conjecture on Sphere Packings with Kissing Number Twelve
- Mathematics in the Age of the Turing Machine (survey paper on computers in mathematics, Lecture Notes in Logic (CUP) in commemoration of the centennial of Turing's birth)
- On the Reinhardt Conjecture (Vietnam Journal of Mathematics)
- Dense Sphere Packings: a blueprint for formal proofs (book, Cambridge University Press, available on Amazon), errata
- The Strong Dodecahedral Conjecture and Fejes Toth's Conjecture on Sphere Packings with Kissing Number Twelve, (arXiv preprint, to appear Fields Institute, 2013)
- (with A. Solovyev) Efficient formal verification of bounds of linear programs, in LNCS 6824
Research (Representation theory, formal proofs, motivic integration, discrete geometry) - The Kepler Conjecture (What is the densest arrangement of spheres in space?)
- Flyspeck Project Page (the Formal Proof of the Kepler Conjecture)
External Search CausesJoin The Boycott of ElsevierRemember "Don't use manual procedures" -Andrew Hunt and David Thomas and ... "don't rely on social processes for verification" -David Dill License This site is licensed under creative commons. Help yourself! |