# Mathematicians spark debate with 13 GB proof for Erdős problem

## Try fitting THAT in the margins, math wonks

When Pierre de Fermat famously complained that he didn't have space to write the proof of his famous “Fermat's Last Theorem”, he only ran out of space of the margin of a book. Now, a pair of mathematicians at the University of Liverpool in the UK have produced a 13GB proof that's sparked a debate about how to test it.

The mathematicians, Alexei Lisitsa and Boris Konev, were looking at what's called the “Erdős discrepancy problem” (it's appropriate to point to Wikipedia, for reasons you'll catch in a minute).

New Scientist describes the problem like this:

“Imagine a random, infinite sequence of numbers containing nothing but +1s and -1s. Erdős was fascinated by the extent to which such sequences contain internal patterns. One way to measure that is to cut the infinite sequence off at a certain point, and then create finite sub-sequences within that part of the sequence, such as considering only every third number or every fourth. Adding up the numbers in a sub-sequence gives a figure called the discrepancy, which acts as a measure of the structure of the sub-sequence and in turn the infinite sequence, as compared with a uniform ideal.”

For any sequence, Paul Erdős believed, you could find a finite sub-sequence that summed to a number bigger than any than you could choose – but he couldn't prove it.

In this Arxiv paper, the University of Liverpool mathematicians set a computer onto the problem in what they call “a SAT attack” using a Boolean Satisfiability (SAT) solver. They believe they've produced a proof of the Erdős discrepancy problem, but there's a problem.

After six hours, the machine they used – an Intel i5-2500 running at 3.3 GHz with 16 GB of RAM – produced what they offer as a proof, but it's inconveniently large, at 13 GB. A complete Wikipedia (see, I told you it was relevant) download is only 10 GB.

As New Scientist points out, that raises a different problem: how can humans ever check the proof. However, at least one mathematician NS spoke to said “no problem”: after all, other computers can always be deployed to test the proof. ®

### Other stories you might like

• DigitalOcean tries to take sting out of price hike with \$4 VM
Cloud biz says it is reacting to customer mix largely shifting from lone devs to SMBs

DigitalOcean attempted to lessen the sting of higher prices this week by announcing a cut-rate instance aimed at developers and hobbyists.

The \$4-a-month droplet — what the infrastructure-as-a-service outfit calls its virtual machines — pairs a single virtual CPU with 512 MB of memory, 10 GB of SSD storage, and 500 GB a month in network bandwidth.

The launch comes as DigitalOcean plans a sweeping price hike across much of its product portfolio, effective July 1. On the low-end, most instances will see pricing increase between \$1 and \$16 a month, but on the high-end, some products will see increases of as much as \$120 in the case of DigitalOceans’ top-tier storage-optimized virtual machines.

• GPL legal battle: Vizio told by judge it will have to answer breach-of-contract claims
Fine-print crucially deemed contractual agreement as well as copyright license in smartTV source-code case

The Software Freedom Conservancy (SFC) has won a significant legal victory in its ongoing effort to force Vizio to publish the source code of its SmartCast TV software, which is said to contain GPLv2 and LGPLv2.1 copyleft-licensed components.

SFC sued Vizio, claiming it was in breach of contract by failing to obey the terms of the GPLv2 and LGPLv2.1 licenses that require source code to be made public when certain conditions are met, and sought declaratory relief on behalf of Vizio TV owners. SFC wanted its breach-of-contract arguments to be heard by the Orange County Superior Court in California, though Vizio kicked the matter up to the district court level in central California where it hoped to avoid the contract issue and defend its corner using just federal copyright law.

On Friday, Federal District Judge Josephine Staton sided with SFC and granted its motion to send its lawsuit back to superior court. To do so, Judge Staton had to decide whether or not the federal Copyright Act preempted the SFC's breach-of-contract allegations; in the end, she decided it didn't.

• US brings first-of-its-kind criminal charges of Bitcoin-based sanctions-busting
Citizen allegedly moved \$10m-plus in BTC into banned nation

US prosecutors have accused an American citizen of illegally funneling more than \$10 million in Bitcoin into an economically sanctioned country.

It's said the resulting criminal charges of sanctions busting through the use of cryptocurrency are the first of their kind to be brought in the US.

Under the United States' International Emergency Economic Powers Act (IEEA), it is illegal for a citizen or institution within the US to transfer funds, directly or indirectly, to a sanctioned country, such as Iran, Cuba, North Korea, or Russia. If there is evidence the IEEA was willfully violated, a criminal case should follow. If an individual or financial exchange was unwittingly involved in evading sanctions, they may be subject to civil action.

• Meta hires network chip guru from Intel: What does this mean for future silicon?
Why be a customer when you can develop your own custom semiconductors

Analysis Here's something that should raise eyebrows in the datacenter world: Facebook parent company Meta has hired a veteran networking chip engineer from Intel to lead silicon design efforts in the internet giant's infrastructure hardware engineering group.

Jon Dama started as director of silicon in May for Meta's infrastructure hardware group, a role that has him "responsible for several design teams innovating the datacenter for scale," according to his LinkedIn profile. In a blurb, Dama indicated that a team is already in place at Meta, and he hopes to "scale the next several doublings of data processing" with them.

Though we couldn't confirm it, we think it's likely that Dama is reporting to Alexis Bjorlin, Meta's vice president of infrastructure hardware who previously worked with Dama when she was general manager of Intel's Connectivity group before serving a two-year stint at Broadcom.