An App Proof

That is “app” as in an on-line application

[ Leo Stein ]

Leo Stein is an assistant professor in the department of Physics and Astronomy at the University of Mississippi. His research interests include general relativity from an astrophysical standpoint.

Today I want to share an unusual proof of his.

Mathematics and complexity theory are all about proving theorems. Most of the time, so far, we prove the old way: we write out a humanly readable proof. At least we hope the proof is readable. Some of the time, we use a computer to check or even create the proof. Sometimes we do extensive numerical computations, but these are not proofs.

Solving Quadratic Equations

I have known, as I am sure you do, forever that a quadratic equation can be solved in closed form. That is

has the two solutions

I have discussed this before here and its relationship to the World’s Fair in Flushing Meadows.

A natural question is: Are square roots needed in any formula for quadratic equations? The answer is “Yes”.

Theorem 1 There does not exist any continuous function from the space of quadratic polynomials to complex numbers which associates to any quadratic polynomial a root of that polynomial.

Corollary 2 There is no quadratic formula built out of a finite combination of field operations and the functions , and the coefficients of the polynomial.

The corollary uses the basic fact that are continuous functions. Note that each has a single branch on complex plane, whereas radicals and the logarithm function do not. So how do we prove the theorem?

An App Based Proof

Here is a novel, I think, proof that uses an app. Stein has written the app and it is here. He explains how to use it. I strongly suggest that you try this yourself.

To get a feel for all this, drag the coefficient to and the coefficient to . You should have two real roots in root space (one at , the other at ). Let’s call the negative root, and the positive root. Now move the coefficient around in a small loop (i.e. move it around a little bit, and then return it to where it started). Note that the roots move continuously, and then return to their original positions. Next, move in a big loop (big enough that it orbits around ). Something funny happens: the roots and switch places.

Leo Goldmakher says here:

Pause and think about this for a second. This is really, really weird.

Here is one immediate consequence of this observation:

Theorem 3 There does not exist any continuous function from the space of quadratic polynomials to complex numbers which associates to any quadratic polynomial a root of that polynomial.

And so the corollary follows.

A Standard Proof

Goldmakher writes out a more conventional proof in his paper titled Arnold’s Elementary Proof Of The Insolvability Of The Quintic. He also shows the following theorem:

Theorem 4 Fix a positive integer . Any quintic formula built out of the field operations, continuous functions, and radicals must have nesting of level more than .

This says that there can be no fixed formula for fifth degree, quintic, polynomials. Of course, this follows from Galois theory, but his proof uses just calculus. The Arnold is Vladimir Arnold.

Open Problems

Do you know other cases of an app with animation conveying the essence of a mathematical proof? This means more than “proofs in pictures” or “proofs without words”—the animation and interactivity are crucial.

Advertisements

Internet, Dogs, and the ABC Conjecture

An inappropriate comment on the ABC conjecture

Joseph Oesterlé and David Masser are famous for their independent discovery of the ABC conjecture.

Today I want to point out an unfair comment about their discovery.

Making Elections Safe

A new proof that MAJORITY is not in .

[ Rich DeMillo ]

Rich DeMillo is a strong leader, a famous researcher, and a long-time best friend. Proof: He was the first CTO at HP and was the Dean of Computing at Georgia Tech; He helped created mutation a powerful software testing method and did seminal work in complexity theory. The last is clear.

Today I want to talk about his recent work on voting systems.

The 2020 election is over a year away, yet it is on our collective minds. People voice concerns everyday on social media, on TV, on cable, in print, everywhere. Their concerns are that our next national election will be compromised. Rich has turned his concern into activism: he is working hard to make elections trusted in general and the 2020 election in particular.

Rich is scheduled to give a talk this coming Monday, May 13, at Georgia Tech. I wish I could be there, but cannot. I do plan to watch the video of his presentation—see here. The talk is based on his recent paper joint with Andrew Appel and Philip Stark titled, “Ballot-Marking devices (BMDs) cannot assure the will of the voters.” As an aside, their paper (ADS) has already generated measurable interest—it’s been downloaded over times and viewed over times.

What Makes A Good Election?

There are several criterion that a “good” election should have.

• During the voting: Only eligible voters can vote.

• During the tabulation: Each voter gets exactly one vote.

• After the election: Each vote remains secret.

Rich says in his talk abstract:

Many people believe that, in an Internet-enabled world, secure, safe voting should be easy to achieve. For example, using known cryptographically secure protocols (maybe even blockchains), a secure website might be developed to relieve voters of the burden of driving to a polling place on election day.

This belief is wrong. Elections are hard—impossible?—to safeguard. A U.S. national election is the union of about ten thousand local elections. Each has different rules and protocols, which makes safeguarding the national election difficult.

• During the voting: Who votes is subject to human decisions? People must prove they are eligible voters. Even computer identification is subject to bias.

• During the tabulation: Counting is usually a combination of human and computer systems. The former make errors and as do the latter. Computers can have bugs or can be hacked by adversaries.

• After the election: Since records are usually kept of the voting, they must be safeguarded to avoid disclosing how someone voted.

The last point is central. There must be a record of the votes to allow audits after the election is over. We must be able to audit and check that the tabulation was correct. This is the central question that Rich and his co-authors discuss. We will turn to this issue in a moment.

Before that I note that keeping a vote secret is impossible in an absolute sense. Suppose that you vote “yes” in some district. After the election suppose that the count in that district is made public, as it usually is. Say of the votes were yes. Then clearly information is leaked about how you voted.

How Are Votes Recorded?

There are two main ways to record votes. One method is to have voters hand-mark their ballots, in the old-fashioned way. It is simple, cheap, and not 21st century. Hand-marked ballots can be read by automatic scanners, at least in principle. A difficulty is voters are human and may mark their ballots incorrectly. They may miss a box, or mark two boxes, or make some other mistake. What if the voter is instructed to:

Select two of the following six choices.

There can be other difficulties: Some voters may have special needs and may require instructions to be in a large type font, for example.

Another recoding method is to have voters use a device to print their paper ballots. These are cleverly called Ballot Marking Devices (BMDs). The name sounds slightly strange to me; there is an alternative name, electronic ballot markers (EBMs).

The authors, ADS, argue that BMDs are dangerous. Such devices can fail, they argue, and not protect the election. The BMDs rely on software, complex special purpose software, and thus are subject to bugs, errors, mistakes, and to active attacks by adversaries.

A BMD device takes input from a voter and then prints out a paper ballot. Often the ballot will contain a machine-readable bar code. This is so scanners can more easily read the paper ballots, later. The problem, the danger, is that most voters cannot tell if a bar code is correct or not. An attacker need only have the BMD confirm that you voted say “yes” and print a ballot that says “yes”. Then the attacker has the BMD cheat you by printing a bar code that says “no”. This is a nasty attack, which is hard to stop. The ADS team discusses this and related problems with BDMs.

Mathematics and Voting

Can complexity theory help us design better elections? Unclear. Can election theory help us understand complexity theory? Perhaps.

Elections Inform Complexity Theory

Theorem 1 The Election Hardness Axiom implies that the MAJORITY function cannot be computed by a polynomial size constant depth Boolean circuit of NOT, AND, and OR gates.

That is, the MAJORITY function is not in . What is the Election Hardness Axiom? It is the empirical fact that there is no practical way to compute who won an election. The MAJORITY function is the tabulation of votes: The outcome of an election is the same as computing the MAJORITY function of the votes—“yes” is a and “no” is a .

Okay we are kidding. But not completely. Suppose that MAJORITY function were in . Then a series of decisions of the form:

The tabulators have looked at the following ballots and we agree that there is a “yes” vote in ballot .

Complexity Informs Elections

Rich, in his talk abstract, states that it is unlikely that crypto theory could be used to create trusted elections. His reason is voters will not trust elections that rely on crypto results. I agree. But I wonder if ideas from theory could be useful. Here are two high-level thoughts.

There is a vast literature on computing in the presence of faults. Usually “faults” are thought to occur at the nano level: the faults are due to hiccups in electronics. What if the faults came from errors in the counting of votes? What if the faults were at the macro level? That is at the level of human decisions? Perhaps we will revisit this in the future.

There is a vast literature on computing as a “game”. An election is usually viewed as being run by some trusted party. This could be replaced by assuming that the election is a game. Imagine two parties D and R. As the tabulation is performed D and R can challenge each other. They interact as in game. Could this help make the election trusted? Perhaps we will revisit this too in the future.

Open Problems

Can we elections be trusted? Can we formalize the connection between election and ? Could this connect be useful? Can theory help with future elections?

The Network Coding Conjecture Is Powerful

More hard Boolean functions

Peyman Afshani, Casper Freksen, Lior Kamma, and Kasper Larsen (AFKL) have a recent paper which we just discussed.

Today Ken and I will update our discussion.

Their paper assumes the network coding conjecture (NCC) and proves a lower bound on the Boolean complexity of integer multiplication. The main result of AFKL is:

Theorem 1 If the NCC is true, then every Boolean circuit that computes the function has size .

The function is: Given an -bit number and a number so that , compute the -bit product of by :

This is a special case of the integer multiplication problem. In symbols it maps and to , as in our photo above.

Our point, however, is not about integer multiplication. Nor even about NCC—no knowledge of it will be needed today, so read on even if you are not aware of NCC. No. Our point is that a whole lot of other Boolean functions would inherit the same circuit lower bound as . And several aspects of that seem troubling.

Sedgewick Wins An Award

An award for educational writing

[ ACM ]

Robert Sedgewick is the 2018 recipient of the ACM Outstanding Educator Award.

Today we congratulate Bob on this wonderful honor.

Network Coding Yields Lower Bounds

Practice leads theory

Peyman Afshani, Casper Freksen, Lior Kamma, and Kasper Larsen have a beautiful new paper titled “Lower Bounds for Multiplication via Network Coding”.

Today we will talk about how practical computing played a role in this theory research.

The authors (AFKL) state this:

In this work, we prove that if a central conjecture in the area of network coding is true, then any constant degree boolean circuit for multiplication must have size , thus almost completely settling the complexity of multiplication circuits.

Why Check A Proof?

Why check another’s proof?

[Russell and Whitehead ]

Bertrand Russell and Alfred Whitehead were not primarily trying to mechanize mathematics in writing their famous book. They wanted to assure precision and certainty in proofs while minimizing the axioms and rules they rest on. They cared more about checking proofs than generating theorems. By the way: They are listed in the order Whitehead and Russell on the book. See this for a discussion about the importance of the order.

Today Ken and I thought we would add a few more thoughts on why proofs get checked.