Ethics in Mathematics

Here are some resources for Ethics in Mathematics.



Architecture of proof assistants

Have you ever wondered what mathematical proof assistant to use? Here
is a quick guide to their architectures.

HOL Light


HOL Light has an exquisite minimal design. It has the smallest kernel
of any system. John Harrison is the sole permanent occupant, but he
is very welcoming to guests.


tower-cranes-airport-istanbulLean is ambitious, and it will be massive. Do not be fooled by the name.
Construction area keep out” signs are prominently posted on the
perimeter fencing.


Moscow ministry of foreign affairsOnce the clear front-runner, it now shows signs of age. Do not expect
to understand the inner workings of this system unless you have been
trained in Warsaw.



Coq is built of modular components on a foundation of dependent type theory. This system has grown one PhD thesis at a time.


Is-Hearst-Tower_619X313Designed for use with multiple foundational architectures, Isabelle’s early
development featured classical constructions in set theory. However,
its largest modern tower is HOL.


Squatters in Venezuela

Does this really work? Defying expectations, Metamath seems to function
shockingly well for those who are happy to live without plumbing.


Formal Abstracts – a Vision

The Formal Abstracts (FABSTRACTS) project will establish a formal abstract service that will express the results of mathematical publications in a computer-readable form that captures the semantic content of publications.

Specifically, the service will

  • give a statement of the main theorem of each published mathematical paper in a language that is both human and machine readable.
  • link each term in theorem statements to a precise definition of that term (again in human/machine readable form), and
  • ground every statement and definition in the system in some foundational system for doing mathematics (the Lean theorem prover).

What is the long-term vision for Formal Abstracts (FABSTRACTS) in mathematics?

FABSTRACTS enables machine learning in math

Many mathematicians dream that computers will someday fundamentally
transform how mathematics is practiced, and FABSTRACTS expresses
in concrete terms how that transformation might be achieved.

Automation of mathematics has been a major aim of artificial
intelligence from its inception. This broad aim includes all aspects
of mathematical activity such as conjecturing, generating examples,
finding counterexamples, computing, learning,
collaborating, proving, generalizing, refereeing and checking,
searching, exploring, and transforming the literature.

For many of these activities, it is important or even essential to
have a machine-readable semantic representation of mathematical
objects. This is achieved by FABSTRACTS.

We foresee tools for exploration such as a Google Earth for
mathematics, providing an intuitive visual map of the entire world of
mathematics, combining formal abstracts, computation, and other
networked content — all displayed at user-selected resolution.

It gets easier

Just as the FABSTRACTS project will enable AI in mathematics, the
development of AI will enable FABSTRACTS.

Looking forward beyond the challenging initial groundwork to get
FABSTRACTS up and running, the generation of formal abstracts will
become nearly fully automated. The production of formal abstracts
will become easier and more efficient with every passing year.

Tools for the natural language processing of mathematics are under
development. As these tools develop, automation will replace the
manual preparation of formal abstracts. Automation will make it feasible
to construct hundreds of thousands (and eventually millions)
of formal abstracts.

For example, Kofler and Neumaier have developed a powerful parser for common mathematical language, and Neumaier is currently rewriting some of his
published math books in multilingual editions so as to be parsed and
translated by their software.  In other promising work,
Ganesalingam’s thesis gave a brilliant linguistic analysis of the
language of mathematics. The current Naproche (Natural language
Proof Checking) system accepts a rich subset of mathematical language
including TeX-style formulas.

We expect mathematicians to be able to supply their own formal abstracts
in a structured English format, which will be parsed and translated to the Lean language.

We foresee future cooperation between FABSTRACTS and a major math
abstract service (such as zbMATH or MathSciNet).
The abstract service will provide statements of
theorems from publications in a form suited for fast formal
abstraction, and with FABSTRACTS offering enhancements to those services.

Progress in document analysis will eventually permit the automated
extraction of formal abstracts directly from the documents (building
on the work of M. Suzuki and collaborators at Kyushu University).

FABSTRACTS as a permanent service

FABSTRACTS will become integrated with the workflow of
several tens of thousands of mathematicians.

We foresee a TeX package that allows mathematicians to cite formal
definitions and theorem statements for the convenience of readers, and
for the automatic processing of texts:

Let $M$ be a \formal{banach manifold}[]. %TeX

We foresee further integration of FABSTRACTS with computation (in the
style of the current SageTeX package, which performs SageMath
computation and graphics from within a TeX document).

We foresee the translation of formal abstracts into many languages
and formats. Lewis has constructed a two-way bridge between Mathematica and Lean. Computer programs already exist that give automated translations between some of the major proof assistants. The work of Kohlhase, Rabe, and
their coworkers develops general infrastructure for the translation of
formal mathematics between different systems. The point is
that before we translate, we first need any formal representation,
and that is achieved by FABSTRACTS.

There are many expected applications,
including training sets for machine learning, enhancement of automated
theorem proving technologies, machine translation of mathematical
texts into foreign languages, detecting errors in the mathematical
literature, and intelligent mathematical search

Finally, we foresee that FABSTRACTS will inspire a broader movement
for the increased precision in science, with mathematicians taking up
the challenge to formalize the proofs of formal abstracts, and
scientists finding precise ways to give formal expression to the
objects of their research.

Formal Abstracts in Mathematics

The Sloan Foundation has announced funding for a project to develop Formal Abstracts in Mathematics (FABSTRACTS).


To develop software and services for transforming mathematical results as they appear in journal article abstracts into formally structured data that machines can read, process, search, check, compute with, and learn from as logical statements.


  1. Careful and curated capture of at least 5,000 formal definitions and 2,000 formal abstracts of theorems.
  2. A “training set” that allows for Machine Learning and other automation techniques to improve the efficiency in capturing formal abstracts by at least 30%.
  3. A functional service for mathematicians to search and contribute formal abstracts.
  4. Wide adoption of the service as measured by thousands of unique uses of the service in the first six months it is available.

Bertrand Russell Prize of the AMS

(The following interview originally appeared in the Line  about the Bertrand Russell Prize of the AMS)

Professor Thomas C. Hales of the University of Pittsburgh has established the Bertrand Russell Prize of the AMS. The prize looks beyond the confines of the profession to research or service contributions of mathematicians or related professionals that promote good in the world. Prof Hales talked about his inspiration for the prize.

1. What about Bertrand Russell inspired you to endow a prize in his name?

Russell wrote that in his youth, “mathematics was my chief interest and, and my chief source of happiness.” Yet, his legacy extends far beyond mathematics. On the whole, Russell’s writings promote rational analysis in pursuit of humanitarian ends. The prize has related aims.

2. If you were to award a prize to Bertrand Russell, which of his achievements would you recognize?

I would award Russell a prize for his efforts during the Cold War to warn the world of the dangers of nuclear catastrophe.

The Russell-Einstein manifesto, which was published in 1955, led to the founding of the Pugwash conference, an organization devoted to the reduction of nuclear weapons and to the social responsibility of scientists.

In 1995, the Nobel Peace Prize was shared by Joseph Rotblat (one of the 11 signatories of the Russell-Einstein manifesto) and the Pugwash conference for their work.

3. In what ways have your mathematics intersected those of Russell’s?

Bertrand Russell is the father of type theory.  Historically, there were two resolutions of Russell’s paradox: axiomatic set theory and the theory of types. There is a direct chain of influence from Russell’s type theory, to Alonzo Church’s simply-typed lambda calculus, to Dana Scott’s logic of computable functions (LCF), to higher-order logic (HOL). The formal proof of theorems in HOL is one of my primary research interests.

4. What is an example from the past of a person, a mathematical achievement or application you feel might warrant this prize?

I will pick an old example that has not lost its relevance.

Norbert Wiener, the creator of cybernetics and the mathematical theory of communication (with Shannon), campaigned for the ethical use of these technologies. With remarkable prescience, Norbert Wiener educated the public about the social disruptions (such as widespread unemployment) that would result from automation, unless mitigated through sound public policy.

More about the Prize

Prize Description:  This prize looks beyond the confines of our profession to research or service contributions of mathematicians or related professionals to promoting good in the world.  It recognizes the various ways that mathematics furthers fundamental human values.

Prize Details:  The $5,000 prize will be awarded every three years.

About this Prize:  The mission of the AMS includes

  1. promoting the uses of mathematical research,
  2. advancing the status of the profession of mathematics, and
  3. fostering an awareness and appreciation of mathematics and its connections to other disciplines and everyday life.

This prize, proposed and funded by Thomas Hales, is designed to promote these goals.  Mathematical contributions that further world health, our understanding of climate change, digital privacy, or education in developing countries, are some examples of the type of work that might be considered for the prize.

Nominate a Candidate



Bad Packings

Thomas C. Hales (Pittsburgh)

[This blog post is based on a colloquium I gave in the Pitt math department on February 3, 2017. The arXiv paper (1703.01352) giving technical details appeared March 7, 2017.]

Some shapes fill the plane more efficiently than others.

For example, some shapes tile the plane, so that there is no unoccupied space. Shapes that tile include the equilateral triangle, the square, the parallelogram, and the regular hexagon. Fish also tile the plane, as shown by Escher.

Shapes that do not tile the plane include circles and pentagons. It is known that the optimal density of a circle packing in the plane is \pi/\sqrt{12}\approx 0.9069. The pentagon packing problem was solved by Kusner and me in 2016. The optimal density is about 0.921.

When studying optimal packing densities, we exclude non-convex disks because otherwise we could hollow out the interior of the disks so that its best packing has arbitrarily small density. For example, hollowed out squares have low packing density.


Central Symmetry

A region in the plane is centrally symmetric if it is the same when rotated by 180 degrees. A camel is not centrally symmetric because we can tell which camel is upside down. Similarly,  triangles and generic quadrilaterals are not centrally symmetric.

Circles and parallelograms are centrally symmetric. Escher’s hands give an algorithm for drawing centrally symmetric figures.

Enter Reinhardt

This blog post is about the problem of bad packings: what centrally symmetric convex disk in the plane has the property that its densest packing is the worst? Reinhardt asked this question and conjectured an answer in 1934. The conjecture is still open.

The problem can be described as follows. A contract stipulates that a miser must make a payment with a tray of identical gold coins filling the tray as densely as possible. The contract requires the coins to be convex and centrally symmetric. What shape coin should the miser choose to part with as little gold as possible?

The answer is not a pentagon for two reasons: its best packing beats the circle, and because the pentagon is not centrally symmetric.

Tiling with hexagons

Centrally symmetric hexagons are obtained by cutting two opposite corners from a parallelogram.  Centrally symmetric hexagons always tile the plane.


Fejes Toth found the best way to pack any centrally symmetric disk: put it in the smallest possible centrally symmetric hexagon, then tile the plane with the hexagons. (In degenerate cases, the hexagon might become a parallelogram.)  Reinhardt himself only considered lattice packings when he formulated his problem, but because of Fejes Toth’s result, the non-lattice and lattice densities are the same, so this does not matter.

The density is the ratio of the area of the disk to the area of the hexagon. This ratio is not affected by rescaling both the disk and the hexagon by the same factor. To normalize the problem, we rescale the hexagons so that they have area \sqrt{12}. This is convenient because it is the area of the smallest centrally symmetric hexagons that contain a circle of radius 1.

We see that Fejes Toth’s strategy works for circles: we obtain the densest packing of circles by fitting each circle as tightly as possible into a hexagon, then tiling the hexagons.

Could the answer to the Reinhardt problem be long and skinny, like the ellipses shown below? A simple argument allows us to restrict to disks that are close to circular. An invertible linear transformation of the plane does not change the ratio of areas (and hence the density). A linear transformation can be applied to make answer to the Reinhardt problem nearly round. In fact, by linear transformations, without loss of generality the boundary of the disk solving the Reinhardt problem passes through the six vertices of a regular hexagon.


Clipping Squares down to Octagons

Here is how Reinhardt might have discovered his conjecture. One way to search for the worst disk is to start with a square and start cutting away unneeded portions (in a centrally symmetric way). Let’s cut away two opposite corners. This doesn’t help, because a square with two clipped corners is a centrally symmetric hexagon and still tiles.

So let’s cut away all four corners of a square. As we cut away more and more from the corners,  its best packing density becomes worse and worse. Except if we cut away too much, we get smaller square and we are back where we started. So let’s stop midway at an octagon. Small further improvements are possible if you make tiny clips at the corners to smooth out the corners of the octagon.

Reinhardt’s conjecture (1934): The smoothed octagon is the worst centrally symmetric shape for packing.

This conjecture is still open.

Reinhardt made an important observation. A shape can be clipped further (and so is not the worst) unless a centrally symmetric hexagon of smallest area passes through each point of the boundary. Reinhardt conjectured that the optimal smoothing of the corners is by arcs of hyperbolas.


This means that the solution to the Reinhardt problem, whatever it is, is hexagonally symmetric in this sense: each point on the boundary can be associated with five other points, for a total of six points.  If we take any of these sets of six points and draw the tangents to the curve at these six points, we get a centrally symmetric hexagon, and its area does not depend on the six points.  We can imagine this as an Escher print with six hands in a ring drawing the figure.

The smoothed octagon has this hexagonal symmetry. (Hexagonal symmetry is a surprising property of an octagon.)  To draw the smoothed octagon with six hands, at any moment, two opposite hands are drawing rounded corners and the remaining four hands are drawing straight edges.    Greg Egan has produced some spectacular animated graphics of this.  The density of the packing does not change as the smoothed octagons roll.


The circles roll in a circle packing in the similar way as the smoothed octagons roll in a packing, except that as the circles roll, there is no visual change in the packing because of their symmetry.

Digression: Ulam conjecture

We can ask the same question in three dimensions: what is the worst shape for packing?

Ulam conjectured that in three dimensions the sphere is the worst shape for packing. Nobody knows if this is true (but some recent progress has been made). The conjecture first became known through a column by Martin Gardner.

Why is the Ulam problem hard? You first have to solve the sphere packing problem to know the density of sphere packings. Then you have to show everything else is worse.  In that sense, the Reinhardt/Ulam problem is much harder than any packing problem.

The sphere packing problem has only been solved in dimensions 2,3,8,24. (For more about packings in 8 and 24 dimensions, see Cohn’s article.)

Some non-Euclidean geometry

(I’m going to make a few digressions, but we will eventually tie up the loose ends.)

In his Elements, Euclid proposed the parallel postulate for the geometry of the plane: given a line L and a point not on that line, there exists a unique line through the point that is parallel to L.

Students of Euclid tried for centuries to give a proof of the parallel postulate. Finally, mathematicians started to believe that no proof of the parallel postulate is possible.

To prove that no proof of the parallel postulate is possible, it was necessary to construct a model of non-Euclidean geometry. In these models, all of the fundamental postulates hold except for the parallel postulate, which fails. In these models, the meaning of primitive terms such as point and line is changed.

Eventually several models of non-Euclidean geometry were found.

The first was the upper-half plane. A second model is the open unit disk. A third model is a branch of the hyperboloid.  As it turns out, all three of these models are useful for the Reinhardt problem.

Dubins car problem

Here is a seemingly unrelated problem in the plane that will turn out to be the key to understanding the Reinhardt conjecture.

The Dubins problem is to take a car that is at a certain position and direction in the plane and navigate it to an ending position and direction in such a way that the absolute value of the curvature of the path is at most 1, and to find the shortest such path.  (See the illustration below.)

In 1957, Dubins showed that the shortest path always consists of straight segments and segments of maximum curvature. According to Wikipedia,

The Dubins path is commonly used in the fields of robotics and control theory as a way to plan paths for wheeled robots, airplanes and underwater vehicles.

Let us juxtapose a solution to the Dubins car problem with its straight edges and circular arcs and a few segments of a smoothed polygon (with its straight edges and hyperbolic-arc-rounded corners). See any similarity?


Dubins car solutions have straight segments and segments of maximum curvature.

Reinhardt’s smoothed octagon has straight segments and segments of maximum curvature, subject to the hexagonal symmetry constraints. (It is an easy fact that the segments of maximum curvature subject to hexagonal symmetry constraints are exactly arcs of hyperbolas.)  We can think of Reinhardt’s problem as a variant of Dubins car problem, where hexagonal symmetry is imposed and the steering wheel turns only to the left.

We now have a well-defined research program to resolve the Reinhardt conjecture: solve the Reinhardt conjecture in the same way that the Dubins car problem was solved.

I’m willing to bet that this 1934 conjecture will soon be solved because of this connection with the Dubins car problem.

Here are some features of the Dubins car problem (and now features of the Reinhardt problem).

  • It is a problem in optimal control theory. Until recently noticing the analogy with Dubins, we did not even know that the Reinhardt problem is an optimal control problem.  It was misclassified for decades as a problem in discrete geometry, which impeded progress towards a solution.
  • It is a bang-bang solution.
  • It is studied using Pontryagin’s maximum principle (PMP). In particular, the smoothed octagon is a Pontryagin extremal.

I will explain each of these points in turn.

A Problem in Optimal Control Theory

An optimal control problem has the form of minimizing the cost of x, where x is a solution to a differential equation that depends on a control function u.  The problem of optimal control is to pick the control function u, such that after solving the differential equation for x with given boundary conditions, the cost of x is minimized.

To make this concrete, here is an example of a control problem that we take from non-Euclidean geometry.

The solution x to the differential equation will be a path in the hyperboloid model of non-Euclidean geometry.  We take the cost of x to be the number we get by integrating the height function on the hyperboloid along the path x.

We take the control function u:[0,T]\to U to take values in an equilateral triangle (shown here with a control stick).  The differential equation is shown, and the coefficients (a,b,c) depend on the control u.


Here is the connection between the Reinhardt problem and non-Euclidean geometry.

Theorem: The solution to this optimal control problem in non-Euclidean geometry gives the solution of the Reinhardt problem. 

The connection between non-Euclidean geometry and bad packings comes through the group SL(2,R) which acts on both the Euclidean and non-Euclidean planes.

In particular (and quite remarkably) the integral of the height function on the hyperboloid is equal to the area of the convex disk D in the plane (up to a fixed constant 1.5).

Also,  the motion along the path x gives the animation of the rolling disks D (in Egan-style animations).

Bang-bang controls

Suppose U is a convex set. A bang-bang control u:[0,T]\to U is one that take values in the set of extreme points of U. A feature of many optimal control problems is that the control that minimizes cost is a bang-bang control.

Here are some standard examples of bang-bang solutions.

Parking a car in a garage in minimal time

The optimal control problem is to park a car in a garage in minimal time.  The car is directly in front of the garage so no turning is needed.  There is a single control variable with range [-1,1] for acceleration (negative values for the break pedal and positive values for the gas pedal).  The optimal solution is bang-bang: to park a car as fast as possible, floor the gas pedal, driving at reckless speed towards the garage. Then just at the moment when  crashing into the back wall of the garage seems inevitable, slam on the breaks, coming to a screeching halt just as the front bumper touches the wall.

Think of bang-bang control as the extreme stuff of Hollywood movies: the bomb that is deactivated just as the timer is reaching zero; the getaway car that evades police on its tail by flying across the train track the instant before the long freight train blocks all further traffic; and the lover who professes love and saves the imperiled relationship when it is all but too late.  (In fact, Bang-Bang is a film title.)

Dubins Car Problem

The circular segments in the Dubins car problem are given by bang-bang controls: the signed curvature is as large or as small as possible.  (However,  The straight-edge segments in Dubins care problem are not bang-bang.  They are called singular arcs.)

Optimal investment strategies

Think of bang-bang optimal financial strategies as the Bill Gates lifetime investment strategy.   Bill Gates the Microsoft CEO ruthlessly builds a corporate empire. Then bang, positions change, and Bill and Melinda Gates the philanthropists plan to donate 95 percent of their wealth to charity.

Many financial investment strategies come as solutions to control problems, jumping from one extreme position to another in an optimal way, according to a bang-bang control.

The smoothed octagon has a bang-bang control

The smoothed octagon has a bang-bang control with finitely many switches.  The smoothed octagon is divided into segments, each of which is  as straight as possible or as curved as possible, with abrupt transitions between the segments.  In terms of the control triangle U described above, the control remains at one vertex for a time, then suddenly jumps to another vertex, and so on.

Enter Pontryagin

Pontryagin gave some necessary conditions that the optimal solution to a control problem must have.

Pontryagin’s conditions are similar to the method of Lagrange multipliers taught to calculus students.  The typical problem is to minimize a function f of x subject to constraints G(x)=0. Lagrange tells us to write \lambda_0 f + \lambda\cdot G with Lagrange multipliers: (\lambda_0,\lambda).  (Generally, \lambda_0=1 and is omitted, but for optimal control which we turn to next, it cannot be omitted.)

The approach is to calculate all critical points and to pick the best. The computation of the multipliers is part of calculating the critical points.

The same idea applies to optimal control, with some small adaptations.  The function f to be minimized is called the cost.  Now, x is a path rather than a point in Euclidean space, and the constraints G(x)=0 are differential equations.  No matter.  Now the multiplier \lambda is also a path rather than a point in Euclidean space, and is itself a solution to a differential equation.

The multiplier \lambda takes values in the cotangent bundle T^*M of M=SL(2) x H, where H is the hyperboloid model.   Cotangent bundles of manifolds are examples of symplectic manifolds, and we can specify the differential equation that \lambda satisfies by giving a real-valued function h on T^*M, called the Hamiltonian.  (Recall that a function h on  has a differential dh, which becomes a vector field on T^*M using the canonical symplectic form.  The integral curves \lambda of that vector field are the solutions to the differential equation.)

Pontryagin maximum principle is a list of  necessary conditions for optimality.  These conditions include an explicit Hamiltonian, which is used to describe the differential equation \lambda must satisfy.  We call \lambda a Pontryagin extremal if it satisfies all the necessary conditions enumerated in the Pontryagin maximum principle.

Theorem: The smoothed octagon is a Pontryagin extremal.

Theorem: The smoothed octagon is a (micro) local minimum.

By micro-local, I mean that the neighborhoods we consider are in the cotangent bundle.

The differential equations are solved exactly and explicitly in Mathematica as part of the proofs. We have used a second derivative test of local minimality.  Briefly put, interval arithmetic was used on a computer to show that the second derivative is positive.

There are in fact infinitely many Pontryagin extrema (smoothed 6k+2-gons) converging to the circle of radius 1. The circle is also a Pontryagin extremal trajectory (a singular arc).  A switch in a bang-bang solution is defined as the jump that the control function u makes from one extreme point of the control space to another.  The the number of switches in these smoothed polygons tends to infinity with k.

If, for example, we could prove that the smoothed 6k+2-gons are the only extrema, (and this seems plausible to me), then that would complete the proof of the Reinhardt conjecture.

There also appear to be infinitely many Pontryagin extrema for local cost maximization (smoothed 6k+4-gons), also converging to the circle. (The  4-gon is degenerate and has corners.)

We graph the cost of the known extrema as a function of the number of straight edges in the smoothed polygon.  The smoothed octagon is the deep dip at n=8.



I have done many calculations in the paper that I have not described in this blog post.

Here is a summary of our main points.

  • In 1934 Reinhardt proposed that the smoothed octagon is the worst packer among centrally symmetric convex disks.
  • The Reinhardt problem can be formulated and studied as a problem in optimal control.
  • In this formulation, the problem is to minimize the total height of paths in the hyperboloid model of non-Euclidean geometry.
  • The shape of the smoothed octagon is completely explained by a bang-bang control.
  • The Reinhardt problem is very similar to other problems in optimal control theory that have been solved (such as Dubins car).
  • The smoothed octagon is a Pontryagin extremal trajectory and a micro-local minimizer.
  • The solution has been confined to a 5-dimensional manifold (which can be searched numerically).
  • I’m willing to wager that the Reinhardt problem will be solved using optimal control theory and that this will happen soon!


Our indebtedness to Escher is apparent.  The spectacular animated graphics of smoothed octagons were developed by Greg Egan.  I have used graphics from a wide varieties of sources.  We acknowledge earlier funding from NSF grant 1104102.

Aristotle’s Tetrahedral Blunder

Aristotle falsely believed that congruent regular tetrahedra tile space:

Among surfaces it is agreed that there are three figures which fill the place that contain them–the triangle, the square and the hexagon: among solids only two, the pyramid and the cube. -De Caelo

The tetrahelix does not extend to a tiling.

(Here the pyramid means the regular tetrahedron.) Even more remarkable than Aristotle’s false belief is that “it took 1800 years for Aristotle’s error to be resolved,” according to the fascinating history documented by Lagarias and Zong. In partial defense of Aristotle, they write that “of course, at the time of Aristotle, methods of geometric measurement and computation were more limited and computers were not available!”

Here we prove that tetrahedra do not tile space, using only math that Aristotle might have understood. This means it took 1800 years more than it should have to set the record straight. Aristotle’s referees should have caught his error before publication!

We limit our proof to the case when the tetrahedra are arranged face-to-face, but a small adaptation of our argument, which we leave to the reader, shows that no tiling is possible even without the face-to-face constraint.

Let us assume for a contradiction that congruent tetrahedra tile space. By placing tetrahedra face-to-face, they are also edge-to-edge and vertex-to-vertex. All the tetrahedra around a fixed vertex V form a Platonic solid with n equilateral triangular faces, where n is the number of tetrahedra meeting at the center V. There are only three Platonic solids with triangular faces: the tetrahedron itself, the octahedron, and the icosahedron. We can immediately rule out the tetrahedron and the octahedron because the angle from the center V to two adjacent vertices of the solid is not an acute angle. (The angle would have to be 60 degrees if part of a tetrahedron tiling). Thus, the tiling must consist of n=20 tetrahedra around the center V, forming an icosahedron.

a diameter of the icosahedron and one face of a tetrahedron around V

To complete the proof we rule out the icosahedron. Consider a plane containing the diameter (the black vertical line) of the icosahedron, and one triangular face as shown. If we let each edge be 1 unit in length, then the diameter is 2, and the vertex V’ has height 1/2 above the center. By symmetry, the icosahedron has five vertices at height 1/2 and five vertices at height -1/2 below center (as shown below).  The distance between the planes at heights +1/2 and -1/2 is 1.  There is a unique point (the orthogonal projection, shown as a blue dot in the figure to the left) on the plane of height -1/2 at distance 1 from V’. This leads immediately to a contradiction: following the two edges on the tetrahedron from V’ to V1 and V2, we find that there are at least two such points!

In the icosahedron, the vertex V’ at height 1/2 cannot have distance 1 from two distinct points V1, V2 at height -1/2.

Acknowledgement: The tetrahelix image is from a post by Brian Hayes