A Special Issue on Formal Proof
Using computers in proofs both extends mathematics with new results and creates new mathematical questions about the nature and technique of such proofs. This special issue features a collection of articles by practitioners and theorists of such formal proofs which explore both aspects.
(pp. 1363)
Thomas Hales
(pp. 1370)
Formal Proof--The Four-Color Theorem
Georges Gonthier
(pp. 1382)
Formal Proof--Theory and Practice
John Harrison
(pp. 1395)
Formal Proof--Getting Started
Freek Wiedijk
By Julie Rehmeyer
Web edition : Friday, November 14th, 2008
Mathematicians develop computer proof-checking systems in order to realize century-old dreams of fully precise, accurate mathematics.
ProofWeb is both a system for teaching logic and for using proof assistants through the web.
ProofWeb can be used in three ways. First, one can use the guest login, for which one does not even need to register. Secondly, a user can be a student in a logic or proof assistants course. We are hosting courses free of charge. If you are a teacher and would like to host your course on this server, send email to proofweb@cs.ru.nl. Thirdly, if teachers do not want to trust us with their students' files, they can freely download the ProofWeb system and run it on a server of their own.
A two-dimensional representation of a Klein bottle--a shape with no inside or outside, just one continuous surface. A true Klein bottle needs at least four dimensions; in other words, it can't be blown from glass. Two- and three-dimensional representations like this one exist to help us visualize the topology, but they are not completely faithful to the original shape. The surface cannot be built in two- or three-dimensional space without self-intersection, as shown here with the "handle" passing through the side of the surface.
Credit: Thomas Banchoff, Brown University, and Davide Cervone, Union College.
Welcome to the Dispersive PDE Wiki! These web pages are intended to present the latest results, conjectures, bibliography, concepts and other material on the local and global well-posedness problems (and related questions) for non-linear dispersive and wave equations. (We also have a more detailed description of this wiki and its purpose.)
Database Reviews and Reports
MathSciNet: Mathematical Reviews on the Web, a Review
Margaret Dominy
Science Librarian
Hagerty Library
Drexel University
dominymf@drexel.edu
Jay Bhatt
Engineering Librarian
Hagerty Library
Drexel University
The Identification of Authors in the Mathematical Reviews Database
Bert TePaske-King
Manager, Bibliographic Services Department
Mathematical Reviews
Norman Richert
Administrative Editor
Mathematical Reviews