Sun Mon Tue Wed Thu Fri Sat
1 2 3 4 5
6 7 8 9 10 11 12
13 14 15 16 17 18 19
20 21 22 23 24 25 26
27 28 29 30
|
The China Labyrinth puzzle
This evening, I used the laser cutter at TkkrLab to create a puzzle (using a SVG
file) based on the The China Labyrinth. Below a picture of the pieces (except for one):
One of the members tried to put the pieces inside the frame where the pieces
were cut from, but failed. There are somewhere between 10^20 and 10^22
solutions to the exact cover program that I use
to estimate the number of solutions. On August 16, I already developed the
program hexapuszleSQ.cpp to
generate the input for exact cover program and to generate an SVG file when
given the filename of the file with the solutions.
Puzzle piece shape designer
Yesterday, a member of TkkrLab suggested that I should
have made the pieces of the puzzle into jigsaw pieces that actually stay
together when locked in. I got this idea to make the shape out of connecting
arcs and made a took to select design it. The tool is given below. The green
line indicates the side of the piece. The grey lines connect with the three
points defining the shape. The points can be moved by clicking with a mouse
and drag them around. The radius of the middle arc can be adjusted with the
slider. When this results in an impossible shape, a message is shown in the
output window. The red lines shows the calculated lines for the connecting
circle to the ends of the side. The output shows the radius and postions of the
three points as percentages of the length of the side. It also calculates the
area above the the side substracted by the area below displayed as a
percentage.
Some notes used for calculating the position of the red lines:
a^2 + (b + x)^2 = (r + x)^2
a^2 + b^2 + 2bx + x^2 = r^2 + 2rx + x^2
2(b - r)x = r^2 - a^2 - b^2
x = (r^2 - a^2 - b^2)/2(b-r)
FLT has been formalized in Lean
Today came the news that FLT has been formalized in Lean by Claude, the AI agent by Antropic. FLT is short of Fermat's Last Theorem,
a famous proposition for which the French mathematician Pierre de Fermat arounf 1637 claimed that he had a proof but that the
proof was large to fit in the margin. Many mathematicians since then have tried
to proof it but it was only in 1994 until Andrew Wiles proved it and formally published it in 1995. Lean is a
mathematical proof assistant and a functional programming language. There are
several other such proof assistants, but currently, Lean is the most popular.
FLT is also the final theorem to be formalize in Freek Wiedijk's famous
list of 100 formalization
challenges and wraps up this 20-year=old benchmark. Lean has become the
proof assistant that is being used to (dis)proof mathematical propositions and
hypothesis with the help of AI agents. There was already work on the way as
part of the Xena project to
formalize FLT in Lean, but now Kevin Buzzard wrote the blog FLT: Anthropic has beaten me to it. But he goes on to explain that
although it is a great achievement, the prove does not follow the proof given
by Willes, which the Xena project wants to formalize and also make a dynamic
document enabling humans to explore the proof. The proof that Clause produced
consists of 13.4 million lines of code and Antropic is probably not going to
work on making it human readable. It is definitely helping the progress of
mathematics now that AI agents are helping to formalize proves in statements
that can be automatically verified and push the use of proof assistance such
as Lean.
Simple Modbus storage server
In the past week, I have been working on a simple server for the Modbus protocol. The server implements a memory store. For a commercial
project I am working on, I have to implement a Modbus client that talks with
some Modbus server. Because I want to test whether this client is working
correctly, I decided to implement a simple server on an ESP32-S3 microcontroller using ESP-IDF with PlatformIO in the
intergrated development environment Visual Studio Code. I also took it as an opportunity to experiment with
the TinyCoPoOS
operating system that I developed almost two years ago and mentioned on
November 17, 2024. I have finished
implementing this in the repository ModbusClient for the 'native' environment with unit-tests, which means not
yet actually tested on an ESP32-S3. That will be next step. I have made some
changes to the TinyCoPoOS operating system that I publised about two years ago
and pushed those to the repository.
Going into the city
I biked into the city with just a shirt because the temperature was around
21° Celsius. At photogalary Objektief, I saw the exhibition De Adem van de Aarde (in English: The Breath of the
Earth) with (digitally manipulated images from) photographs by August Langhout. From there I walked to the galery Beeld & Aambeeld where I saw the exhibition A Transatlantic
Meeting with paintings by Maike Eilers and jewellery by Jillian Moore. I found the paintings interesting but a bit too constructed
as if the artist first creates a digital manipulated image from pictures taken
from nature and then makes a painting of it. I had a quick look at Concordia
where there is a group of four recently graduated international artists who
work on site-specific installations for the GOGBOT festival which opens next Thursday evening. There was not much to
see except two of them working. I walked through the Grote Kerk (Great Church),
which was open due to the European Heritage Days this weekend. It is the oldest building of the city
of which the oldest parts date from around 1200.
The path in SVG uses a different method for specifying an arc than JavaScript.
In JavaScript you specify the coordinates of the center, the radius, the start
and end angle and whether it clock-wise or counter-clock-wise. In the path
command in SVG you can use the 'A' command to draw an arc from the current point to the next
point specifying the size and orientation of an elipse (with three parameters)
and the flags 'large-arc' and 'sweep', and of course the coordinates of the
next point. I also realized that if you want to cut the pieces with a laser
the width of the laser beam is probably two small to make the pieces fit
easily and that you might want to specify the gap between the pieces. With
the below you can specify gap. In the output it produces the values needed for
generating the arc commands in SVG in the form of some code that can be
included in a C(++) program. The position of the points are marked with a dot.
Again going into the city
I first went to Sickhouse where I went
to see, or better, experience the immersive installation Dérive by Alexander
Zanen, where you wearing headphones and a tracker move through the room
while listening to a story. Although I am more of a visual person than an
auditorial person, I did like it. Next, I went to Craft District Enschede to attend the volunteer meet-up for GOGBOT. On the way home, I went to Het
Robson, which was open as part of the European Heritage Days. I saw the exhibition Diana Huijts with works by her. I have a book with prints from her series of lino prints about the
alpha tower (the highest building in Enschede). I was a bit surprised by the
great variation of techniques that were used for all the other works on
display. I also talked a bit with the artists Jet Broekstra and Mark van Loon
from Beeldbouw.
This months interesting links
Home
| August 2026
