jm + proofs   3

Sci-Fi Writer Greg Egan and 4chan anon Math Whiz Advance Permutation Problem | Quanta Magazine
On September 16, 2011, an anime fan posted a math question to the online bulletin board 4chan about the cult classic television series 'The Melancholy of Haruhi Suzumiya'. Season one of the show, which involves time travel, had originally aired in non-chronological order, and a re-broadcast and a DVD version had each further rearranged the episodes. Fans were arguing online about the best order to watch the episodes, and the 4chan poster wondered: If viewers wanted to see the series in every possible order, what is the shortest list of episodes they’d have to watch?

In less than an hour, an anonymous person offered an answer — not a complete solution, but a lower bound on the number of episodes required. The argument, which covered series with any number of episodes, showed that for the 14-episode first season of Haruhi, viewers would have to watch at least 93,884,313,611 episodes to see all possible orderings. “Please look over [the proof] for any loopholes I might have missed,” the anonymous poster wrote.

The proof slipped under the radar of the mathematics community for seven years — apparently only one professional mathematician spotted it at the time, and he didn’t check it carefully. But in a plot twist last month, the Australian science fiction novelist Greg Egan proved a new upper bound on the number of episodes required. Egan’s discovery renewed interest in the problem and drew attention to the lower bound posted anonymously in 2011. Both proofs are now being hailed as significant advances on a puzzle mathematicians have been studying for at least 25 years.
mathematics  internet  math  greg-egan  anime  bizarre  4chan  superpermutation  permutation  proofs 
4 weeks ago by jm
Proving that Android’s, Java’s and Python’s sorting algorithm is broken (and showing how to fix it)
Wow, this is excellent work. A formal verification of Tim Peters' TimSort failed, resulting in a bugfix:
While attempting to verify TimSort, we failed to establish its instance invariant. Analysing the reason, we discovered a bug in TimSort’s implementation leading to an ArrayOutOfBoundsException for certain inputs. We suggested a proper fix for the culprit method (without losing measurable performance) and we have formally proven that the fix actually is correct and that this bug no longer persists.
timsort  algorithms  android  java  python  sorting  formal-methods  proofs  openjdk 
february 2015 by jm
A Brief Tour of FLP Impossibility
One of the most important results in distributed systems theory was published in April 1985 by Fischer, Lynch and Patterson. Their short paper ‘Impossibility of Distributed Consensus with One Faulty Process’, which eventually won the Dijkstra award given to the most influential papers in distributed computing, definitively placed an upper bound on what it is possible to achieve with distributed processes in an asynchronous environment.

This particular result, known as the ‘FLP result’, settled a dispute that had been ongoing in distributed systems for the previous five to ten years. The problem of consensus – that is, getting a distributed network of processors to agree on a common value – was known to be solvable in a synchronous setting, where processes could proceed in simultaneous steps. In particular, the synchronous solution was resilient to faults, where processors crash and take no further part in the computation. Informally, synchronous models allow failures to be detected by waiting one entire step length for a reply from a processor, and presuming that it has crashed if no reply is received.

This kind of failure detection is impossible in an asynchronous setting, where there are no bounds on the amount of time a processor might take to complete its work and then respond with a message. Therefore it’s not possible to say whether a processor has crashed or is simply taking a long time to respond. The FLP result shows that in an asynchronous setting, where only one processor might crash, there is no distributed algorithm that solves the consensus problem.
distributed-systems  flp  consensus-algorithms  algorithms  distcomp  papers  proofs 
november 2013 by jm

Copy this bookmark: