This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project. 2010 Mathematics Subject Classification: 52C17

The relative merits of the methods employed to determine enantiomeric excess (ee) values and absolute configurations of chiral arene and alkene cis-1,2-diol metabolites, including boronate formation, using racemic or enantiopure (+) and (-)-2-(1-methoxyethyl)phenylboronic acid (MEPBA), are discussed. Further applications of: 1) MEPBA derived boronates of chiral mono- and poly-cyclic arene cis-dihydrodiol, cyclohex-2-en-1-one cis-diol, heteroarene cis/trans-2,3-diol, and catechol metabolites in estimating their ee values, and 2) new chiral phenylboronic acids, 2-[1-methoxy-2,2-dimethylpropyl]phenyl boronic acid (MDPBA) and 2-[1-methoxy-1-phenylmethyl]phenyl boronic acid (MPPBA) and their advantages over MEPBA, as reagents for stereochemical analysis of arene and alkene cis-diol metabolites, are presented.

We present a generic digit serial method (DSM) to compute the digits of a real number $V$ . Bounds on these digits, and on the errors in the associated estimates of $V$ formed from these digits, are derived. To illustrate our results, we derive such bounds for a parameterized family of high-radix algorithms for division and square root. These bounds enable a DSM designer to determine, for example, whether a given choice of parameters allows rapid formation and rounding of its approximation to $V$ .

We present a generic digit serial method (DSM) to compute the digits of a real number $V$ . Bounds on these digits, and on the errors in the associated estimates of $V$ formed from these digits, are derived. To illustrate our results, we derive such bounds for a parameterized family of high-radix algorithms for division and square root. These bounds enable a DSM designer to determine, for example, whether a given choice of parameters allows rapid formation and rounding of its approximation to $V$. All our claims are mechanically verified using the HOL-Light theorem prover, and are included in the appendix with commentary.

The HOL Light theorem prover can be difficult to get started with. While the manual is fairly detailed and comprehensive, the large amount of background information that has to be absorbed before the user can do anything interesting is intimidating. Here we give an alternative ‘quick start’ guide, aimed at teaching basic use of the system quickly by means of a graded set of examples. Some readers may find it easier to absorb; those who do not are referred after all to the standard manual.

Algorithmic methods can successfully automate the proof, and even the discovery, of a large class of identities involving sums of hypergeometric terms. In particular, the Wilf-Zeilberger (WZ) algorithm is a uniform framework for a substantial class of hypergeometric summation problems. This algorithm can produce a rational function certificate that can, on the face of it, be used to verify the result by routine algebraic manipulations, independently of the working of the algorithm that discovered it. It is therefore very natural to consider using this certificate to produce, by automated means, a rigorous deductive proof in an interactive theorem prover. However, naive presentations of the WZ method tend to gloss over trivial-looking but rather knotty questions about zero denominators, which makes their rigorous formalization tricky and their ultimate logical justification somewhat obscure. We describe how we have handled these difficulties to produce rigorous WZ proofs inside the HOL Light theorem prover.

With the help of computational proof assistants, formal verification could become the new standard for rigor in mathematics.

We carry out a systematic study of decidability for theories of (a) real vector spaces, inner product spaces, and Hilbert spaces and (b) normed spaces, Banach spaces and metric spaces, all formalised using a 2-sorted first-order language. The theories for list (a) turn out to be decidable while the theories for list (b) are not even arithmetical: the theory of 2-dimensional Banach spaces, for example, has the same many-one degree as the set of truths of second-order arithmetic. We find that the purely universal and purely existential fragments of the theory of normed spaces are decidable, as is the AE fragment of the theory of metric spaces. These results are sharp of their type: reductions of Hilbert's 10th problem show that the EA fragments for metric and normed spaces and the AE fragment for normed spaces are all undecidable.

A special session of the symposium pays tribute to Robin Milner; the session features talks by Robert Harper (Carnegie Mellon University), John Harrison (Intel), and Alan Jeffrey (Bell Labs), and is organised by Andrew D. Gordon (Microsoft Research) and Peter Sewell (University of Cambridge). Robin Milner was born near Plymouth in England. He was educated at Eton College, Windsor, and went up to King’s College, Cambridge, in 1954. In between, his national service was with the Royal Engineers, in Egypt. After university he was first a school teacher and then worked in London as a programmer at Ferranti, an early British computer company. In 1963 he took a job as lecturer at City University, and started research on the side—he never studied for a PhD. In 1968, he moved to Swansea to become a research assistant. He was excited by Scott’s lectures in 1969 in Oxford on domain theory. During this time he learnt about Floyd’s work on verification, and got to know Tony Hoare, and started trying to verify programs. After meeting Zohar Manna during a visit to Carnegie Mellon University, he got a job with John McCarthy at Stanford in 1971. There he built the theorem proving system Stanford LCF, which he would later substantially refine with the addition of a metalanguage (ML) for constructing proofs.

The Distinguished Dissertation series is published on behalf of the Conference of Professors and Heads of Computing and the British Computer Society, who annually select the best British PhD dissertations in computer science for publication. The dissertations are selected on behalf of the CPHC by a panel of eight academics. Each dissertation chosen makes a noteworthy contribution to the subject and reaches a high standard of exposition, placing all results clearly in the context of computer science as a whole. In this way computer scientists with significantly different interests are able to grasp the essentials - or even find a means of entry - to an unfamiliar research topic. Theorem Proving with the Real Numbers discusses the formal development of classical mathematics using a computer. It combines traditional lines of research in theorem proving and computer algebra and shows the usefulness of real numbers in verification.

For purposes of actual evaluation, mathematical functions f are commonly replaced by approximation polynomials p. Examples include floating-point implementations of elementary functions, quadrature or more theoretical proof work involving transcendental functions.

Since the 1990s, Intel has invested heavily in formal methods, which are now deployed in several domains: hardware, software, firmware, protocols etc. Many different formal methods tools and techniques are in active use, including symbolic trajectory evaluation, temporal logic model checking, SMT-style combined decision procedures, and interactive higher-order logic theorem proving. I will try to give a broad overview of some of the formal methods activities taking place at Intel, and describe the challenges of extending formal verification to new areas and of effectively using multiple formal techniques in combination