Dividing a Square into 7 Similar Rectangles

https://johncarlosbaez.wordpress.com/2023/03/06/dividing-a-square-into-7-similar-rectangles/

by ingve • 3 years ago

129 40 3 years ago

johncarlosbaez.wordpress.com

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.

hgsgm5• 3 years ago

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.

phkahler• 3 years ago

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.

actually_a_dog• 3 years ago

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

tromp• 3 years ago

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.

unnah• 3 years ago

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.

hackcasual• 3 years ago

Did my best to match the colors

https://imgur.com/HubwY1d

isaacfrond• 3 years ago

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.

DeathArrow2• 3 years ago

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?

cjfd• 3 years ago

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.

nkrisc• 3 years ago

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.

mkl2• 3 years ago

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).

martincmartin• 3 years ago

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."

lacker• 3 years ago

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.

mik1998• 3 years ago

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.

macrolocal3• 3 years ago

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

anonymoushn• 3 years ago

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

aleks224• 3 years ago

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.

hgsgm5• 3 years ago

With lots of major mistakes along the way.

sdfghswe• 3 years ago

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.

hgsgm5• 3 years ago

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.

Jeff_Brown• 3 years ago

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.

BeetleB• 3 years ago

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...

ogogmad2• 3 years ago

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.

hgsgm5• 3 years ago

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

rssoconnor• 3 years ago

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...

unwind• 3 years ago

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/

wiz21c• 3 years ago

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

DeathArrow2• 3 years ago

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."

elteto• 3 years ago

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

robomartin2• 3 years ago

What is the definition of “similar rectangle”?

shagie• 3 years ago

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.

robomartin2• 3 years ago

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.

Gordonjcp• 3 years ago

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.

Dividing a Square into 7 Similar Rectangles

Related Stories