Selected papers

We apply deep learning based guidance to proof search in the theorem prover E. Using strategies that leverage deep neural networks, we have found first-order proofs of 7.36% of the first-order logic translations of the Mizar Mathematical Library theorems that did not previously have ATP generated proofs. This increases the ratio of statements in the corpus with ATP generated proofs from 56% to 59%.

We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.

TensorFlow is a machine learning system that operates at large scale and in heterogeneous environments. TensorFlow uses dataflow graphs to represent computation, shared state, and the operations that mutate that state. It maps the nodes of a dataflow graph across many machines in a cluster, and within a machine across multiple computational devices, including CPUs, GPUs, and TPUs. TensorFlow supports a variety of applications, with particularly strong support for training and inference on deep neural networks. Several Google services use TensorFlow in production, we have released it as an open-source project, and it has become widely used for machine learning research.

We present a strong solution of the board game pentago, computed using exhaustive parallel retrograde analysis in 4 hours on 98304 ($3 \times 2^{15}$) threads of NERSC’s Cray Edison. At $3.0 \times 10^{15}$ states, pentago is the largest divergent game solved to date by two orders of magnitude, and the only example of a nontrivial divergent game solved using retrograde analysis.

We present a symbolic perturbation scheme for black box polynomial predicates which uses an infinite series of infinitesimal perturbations. Our method is as fast as Emiris and Canny’s randomized linear perturbation scheme, scaling reasonably with the degree of the polynomial even for fully degenerate input. Like Yap’s multiple infinitesimal scheme, the computed sign is deterministic, never requiring an algorithmic restart.

We introduce sculpural forms which replace the resolution dimension of L-systems with a third space dimension, turning a fractal curve into a surface. The distances between the steps of the sequence are scaled exponentially, so that self-similarity of the curves is reflected in self-similarity of the surface.

We present a new BSSRDF for rendering translucent materials. We use a modified diffision theory that accurately couples single and multiple scattering, deriving a novel, analytic, extended-source solution to the multilayer searchlight problem by quantizing the diffusion Green’s function. This allows the application of the diffusion multipole model to material layers several orders of magnitude thinner than previously possible and creates accurate results under high-frequency illumination.

We simulate high resolution cloth consisting of up to 2 million triangles with highly detailed folds and wrinkles. To achieve this level of detail, we use a more accurate model for cloth-object friction, a robust history-based repulsion/collision framework, and distributed memory parallelism. The algorithm is demonstrated by several high-resolution and high-fidelity simulations.

We model highly deformable nonlinear incompressible solids by conserving volume locally near each node in a finite element mesh. Our method works with arbitrary constitutive models, and works with simple linear tetrahedra without locking. We correct errors in volume without introducing oscillations by treating position and velocity in separate implicit solves, and treat treat both object contact and self-contact as linear constraints during the incompressible solve to alleviate issues with conflicting constraints.

We simulate large bodies of water with complex surface effects by combining tall cells with linear pressure profiles with small cells near the interface. The philosophy is to use the best available method near the interface (in the three-dimensional region) and to coarsen the mesh away from the interface for efficiency. We coarsen with tall, thin cells (as opposed to octrees or AMR), because they maintain good resolution horizontally allowing for accurate representation of bottom topography.

We simulate melting and burning solid materials including the resulting liquid and gas. The solid is simulated with traditional mesh-based techniques (triangles or tetrahedra), and the liquid or gas is simulated with modern grid-based techniques. The main advantage of our method is that state of the art techniques are used for both the solid and the fluid without compromising simulation quality when coupling them together or converting one into the other.

We simulate high resolution cloth consisting of up to 2 million triangles with highly detailed folds and wrinkles. To achieve this level of detail, we use a more accurate model for cloth-object friction, a robust history-based repulsion/collision framework, and distributed memory parallelism. The algorithm is demonstrated by several high-resolution and high-fidelity simulations.
SCA 2004

Recent papers

More papers

Recent Posts

More Posts

Greg Egan’s short story “Silver Fire” is about people falling back from secular values. It’s the near future, and organized religion is fading away but “the saccharine poison of spirituaity” is taking its place. The main character is a medical researcher, and most of the plot deals with spirituality in conflict with reliable science. In the background, the reseacher worries about her daughter, who thinks science is boring and much prefers alchemy.


Thanks to a recommendation from Dandelion Mané, I recently read “Sapiens” and “Homo Deus” by Yuval Noah Harari. Both books are wonderful breaths of fresh air and perspective. “Sapiens” is organized as a history of the species Homo Sapiens, tracing from our evolutionary separation from other primates through the cognitive revolution, the agricultural revolution, through the rest of history to the present. From this historical background, “Homo Deus” attempts to extrapolate into the future, in particular asking how our morality and goals will evolve with technology.


The Long Now Foundation is a wonderful organization advocating for long term thinking. Specifically, by long term they mean the next ten thousand years: The Long Now Foundation was established in 01996 to develop the Clock and Library projects, as well as to become the seed of a very long-term cultural institution. The Long Now Foundation hopes to provide a counterpoint to today’s accelerating culture and help make long-term thinking more common.


I make weird typos when writing. Sometimes I substitute an entirely different word in place of the correct one; otherwise times I simply a word. Both kind of typos are more common than misspelling a word, indicating that the typo mechanism is operating at a higher level than the spelling or typing itself. This parallels some of the intuition people have about deep neural networks, which is backed up by pretty pictures of what different neurons see.


(This is an expanded version of a Facebook comment, because Jeremy asked.) Recently I came across an article about opposition to housing development in San Francisco. The headline positions of everyone involved are uninteresting: housing advocates want more affordable housing, housing developers want less. The really interesting bit is more subtle: at one point the developer says they’re still trying to figure out what the community wants and is immediately booed.



  • TensorFlow

    An open source library for large scale machine learning.

  • Eddy

    Autocorrect for Java.

  • Geode

    A utility library of arrays, vectors, matrices, and other mathematical code together with a fast, lightweight python binding layer.

  • Pentago

    Source for the strong solution of pentago, including massively parallel retrograde analysis, approximate forward search, and optimized midgame analysis for website use.

  • Kalah

    Tree search code for kalah, capable of solving up to 5 stones per side.

  • Poker

    Investigations into simplified holdem poker.

  • Fractal

    Various fractal scripts, including partial code for Developing fractal curves.