Dividing a Square into 7 Similar Rectangles | Hacker News Reader

Dividing a Square into 7 Similar Rectangles

johncarlosbaez.wordpress.com

129 pointsingve40 comments

Previously on HN: https://news.ycombinator.com/item?id=34692537

This time a news is that the previously known value for n = 7, 1371, turned out to be incomplete due to the program bug and it is now thought to equal to 1372 instead.

And the bug was quite silly -- it does a simple standard thing (remove obvious symmetries) in a more complicated way (at the end of a long computation, instead of at the start), incorrectly.

Always good to test code with and without such optimizations to verify the results are the same. That's not always practical though for large problems and optimizations that yield significant time savings.

As the saying goes, there are only two hard problems in computer science: naming things, cache invalidation, and off by one errors.

As this incident demonstrates, errors can easily creep into mathematical proofs, even those written by experts. The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness. Especially computer generated proofs should be distrusted unless their output is generated as a computer verifiable. Successful example is Flyspeck, that translated a proof with a large computer generated part into a computer readable one (http://www.proof-technologies.com/flyspeck/)

Computer-readable proofs provide a rigorous and reliable way to verify mathematical results, reducing the likelihood of mistakes and increasing confidence in the validity of mathematical arguments. However, the use of computer-readable proofs is still not widespread in the mathematical community, and it is not yet a standard part of mathematics education.

The tools are ready, it is just that doing the hard work going from a handwritten one to a computer-readable proof is not sufficiently appreciated. It should become more widely used in mathematics, and be incorporated into mathematics education curricula at all levels. Doing so will not only help prevent errors but also promote transparency and reproducibility in mathematical research.

>The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness.

What if the algorithms have errors? What if a cosmic ray flips one bit of memory?

100% accuracy will never be achievable. What might be achievable, though, is a higher degree of confidence than we currently have. Of course, the correctness of algorithms should also have to have a computer validated proof.

> What if the algorithms have errors?

Errors will always happen.

> What if a cosmic ray flips one bit of memory?

Run it several times and compare results until you reach the desired level of statistical certainty.

The tools are not ready. Using proof assistants isn't possible in many areas of maths as the foundational concepts have not yet been built up from fundamental primitives. Even when it is possible, using proof assistants takes far more work, and the proofs are much more verbose and hard for humans to understand. The tools will be ready when the concepts are available for any subfield, when the results are easy to read, and when it takes a reasonable amount of work (ideally it will be faster than doing it by hand).

I agree the tools are not ready because, as you say, the foundational concepts are not yet encoded.

But for OP, the point isn't having humans understand. It's having the computer check the proof. You still use traditional journal papers for communicating the proof to humans. You're just also able to say "The proof has been verified and really is true."

Yes, but humans using the proof assistants need to be able to read and understand the proofs while they are constructing them.

ideally it will be faster than doing it by hand

That's a good point... I agree the tools are not ready. Most computer-assisted tools make it easier to do your work. It's easier to type a five page paper in Word than it is to write it longhand. But for now it's a lot more work to encode a proof in a proof assistant than to just write it up in LaTeX (which I think a lot of people don't realize).

It's not just that the foundational concepts are missing, it's also that proof assistants currently require you to fill in much more detail than human proofs do. You can't just write something like... "this corollary is trivial", or, "since x is a power of 10, obviously cos(x^2) is irrational"; you have to spell out a proof.

Is there a proof here at all? The only thing mentioned in the article is a computation.

With due respect, computer-readable proofs are not very interesting to me as a mathematician. I don't see why we should do it. Reproducibility is not a concern.

I have trouble imagining a mathematician wouldn’t welcome formal verification of eg. the classification of finite simple groups.

Most mathematicians don't care about being exactly right. They only need to not see a contradiction. Since most pure math is not used for anything except more math, mistakes rarely have consequences.

A computer is only a threat, that might find a mistake that humans miss.

This (ahem) contradicts my experience. Most mathematicians I’ve met are excited about formal verification, especially the recent progress toward CFT.

Thompson himself has said he’d like his contributions to the classification of finite simple groups verified in his lifetime, and actively followed/encouraged the Coq implementation of his odd order theorem back in 2012.

> recent progress toward CFT

What's this?

Buzzard's group at ICL, eg. Ashvni Narayanan.

Some steps of the proof are left out. In particular, the correctness of the computation for its purpose is omitted :)

>The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness.

This seems like a strong overstatement. We got by for more than 2000 years without computer-readable proofs, relying on intuition and validation.

With lots of major mistakes along the way.

> As this incident demonstrates, errors can easily creep into mathematical proofs, even those written by experts. The only way to mitigate this is to use computer-readable proofs, (...)

Ironically, computer programs seem to be a lot more error prone than mathematical proofs. Yes, errors in mathematical proofs happen, but they're rare enough that the they're widely reported in the (mathematical) community. Errors in computer programs on the other hand are a virtual guarantee.

Ironically, emails and essays seem to be out more error prone than mathematical proofs...

1. Proofs are intended to be correct. The vast majority of computer programs are intended to be practical, and are far far larger than the largest math proofs. Where correctness matters, computer programs have fewer bugs.

2. Nearly every non-computerized mathematical proof is not even a proof, it is a sketch that requires a lot of hand waving and logical jumps to be interpreted. Likewise, specs have fewer bugs than concrete program, because they aren't complete.

A math professors blew my mind once by telling me that a paper full of errors was still good work and could be salvaged. He went on to say that most good work was like that. In the worst case you end up proving something else, but typically you can prove what you initially set out for. I found that so strange I had to confirm it with another, who concurred.

The reason for this is that mathematical papers are fundamentally about an insight about mathematical objects. The insight typically comes from the mathematician having a deep understanding of the mathematical objects. The theorems are some formalised statement that should be true based on the deep understanding. The proofs are something else entirely, a sequence of steps which combine to verify the theorem but where many steps may result from trial-and-error searching for a path forward. Coming from a good mathemematician, the original insights are much more likely to be correct than the details of the proof steps.

> but they're rare enough that the they're widely reported in the (mathematical) community.

You should ask math professors how often there are errors in papers. Every one has their own ratio, but I've heard numbers as high as 30%. However, the general belief is the results are still correct, so few are worried about building with a pile of cards.

See https://academia.stackexchange.com/questions/143374/extent-o...

A computerised proof checker is much less likely to have a mistake than a typical computer program - or a mathematical proof - because it's extremely simple.

> The tools are ready, it is just that doing the hard work going from a handwritten one to a computer-readable proof is not sufficiently appreciated.

Seems like a perfect task for an LLM trained on English and Idris/Coq/etc

As another example of this, In [1] I've taken a python program for counting (a bound on) the number of iterations needed of the SafeGCD algorithm to compute a modular inverse for any 256-bit (relatively prime) modulus, translated the python into Coq, and proved the implementation correct. Then by running the computation within Coq we produce a theorem about the bounds (e.g. at most 590 iterations needed for the HD variant of the algorithm).

[1] https://blog.blockstream.com/a-formal-proof-of-safegcd-bound...

This is a bit whooosh for my poor head, but very cool to notice that Greg Egan [1] (an SF author definitely represented in my bookshelves) is active in that scene.

[1]: https://gregegan.net/

> we can get two partitions with the same topology where the rectangles have different proportions!

> Here is a picture of the apparently new partition that Daniel Gerbet has found:

I was really looking forward to seeing both partitions with this topology, but the article sadly doesn't highlight the other one.

They do mention that the new partition #1055 has the same topology as partition #1022, and the partitions are numbered in the longer PDF https://math.ucr.edu/home/baez/mathematical/gerbet_partition....

In the shorter PDF it's on page 19, bottom row, second from the left.

Did my best to match the colors

https://imgur.com/HubwY1d

Now we might see this on Leetcode or Hackerrank interviews: "Write a software that takes a number n and outputs the number m, of all different modes a square can be divided into n similar rectangles."

Very cool that Greg Egan did some work on this! He is the author of Permutation City.

Makes me think of Mondrian's paintings :-) Just add the colors :-)

The chart of possible divisions reminds me of those coloured block card things they used for Jet Set Willy's copy protection in the early 80s.

What is the definition of “similar rectangle”?

The ratio of the long side to the short side is the same.

A rectangle that is 2x1 is similar to a rectangle that is 4x2.

The images I saw in the two articles (original and update) don't look like the rectangles have the same aspect ratio. I didn't measure them, so, yes, I could be wrong.

Reply on news.ycombinator.com