We care about your data, and we'd like to use cookies to give you a smooth browsing experience. Please agree and read more about our privacy policy.
Quanta Homepage
  • Physics
  • Mathematics
  • Biology
  • Computer Science
  • Topics
  • Archive

What's up in

computer-assisted proofs

Latest Articles

combinatorics

The Number 15 Describes the Secret Limit of an Infinite Grid

By Kevin Hartnett
April 20, 2023
Comment
Read Later

The “packing coloring” problem asks how many numbers are needed to fill an infinite grid so that identical numbers never get too close to one another. A new computer-assisted proof finds a surprisingly straightforward answer.

Quantized Columns

The Colorful Problem That Has Long Frustrated Mathematicians

By David S. Richeson
March 29, 2023
Comment
Read Later

The four-color problem is simple to explain, but its complex proof continues to be both celebrated and despised.

Illustration of colorful flowchart using raised blocks against a black background
proofs

Proof Assistant Makes Jump to Big-League Math

By Kevin Hartnett
July 28, 2021
Comment
Read Later

Mathematicians using the computer program Lean have verified the accuracy of a difficult theorem at the cutting edge of research mathematics.

Illustration of researchers building and writing a digital library, which helps a humanoid robot do advanced math
foundations of mathematics

Building the Mathematical Library of the Future

By Kevin Hartnett
October 1, 2020
Comment
Read Later

A small community of mathematicians is using a software program called Lean to build a new digital repository. They hope it represents the future of their field.

Illustration of a robot and a human furiously doing math next to each other
artificial intelligence

How Close Are Computers to Automating Mathematical Reasoning?

By Stephen Ornes
August 27, 2020
Comment
Read Later

AI tools are shaping next-generation theorem provers, and with them the relationship between math and machine.

Illustration of floating metal cubes joining together, some of their faces yellow
geometry

Computer Search Settles 90-Year-Old Math Problem

By Kevin Hartnett
August 19, 2020
Comment
Read Later

By translating Keller’s conjecture into a computer-friendly search for a type of graph, researchers have finally resolved a problem about covering spaces with tiles.

Follow Quanta
Facebook
Facebook

Twitter
Twitter

Youtube
YouTube

Instagram
Instagram

RSS
RSS

Newsletter

Past Month

Most Read Articles

This Data is Current Loading...
This Data is Current Loading...
This Data is Current Loading...
The Quanta Newsletter

Get highlights of the most important news delivered to your email inbox

Recent newsletters
Quanta Homepage
Facebook
Twitter
Youtube
Instagram

  • About Quanta
  • Archive
  • Contact Us
  • Terms & Conditions
  • Privacy Policy
  • Simons Foundation
All Rights Reserved © 2023