If I was not so overwhelmed, I could concentrate on writing up my proof of FLT.
It truly is a wonderful proof, most certainly what Fermat found, Once you understand it, you could memorize it.
No, it will not fit on the margin of a page, but I can certainly envision that Fermat could have came up with the proof in his head without writing it down. He was known for not writing things down.
@SearingTruth @tao @standupmaths Give me encouragement to get out of my rut. Please.
Kevin Buzzard (@xenaproject) has just launched his five-year project to formalize the proof of Fermat's Last Theorem #FLT in #Lean4: see his blog post at https://leanprover-community.github.io/blog/posts/FLT-announcement/ and the blueprint at https://imperialcollegelondon.github.io/FLT/blueprint/index.html . As discussed in the blog post, the target is to be able to reduce the proof of FLT to "claims which were known to mathematicians by the end of the 1980s". Hopefully this project will develop many of the foundational theories of modern number theory, and also provide real-world lessons about how to organize a genuinely large-scale formalization project, in particular whether the project is sufficiently modular that many people can make meaningful contributions to the project without having to master all the mathematical prerequisites needed to understand the proof of FLT.
This formalization project is likely to interact with other concurrent projects. For instance, one of the aims of the prime number theorem formalization project I am currently involved in is to establish the Chebotarev density theorem, a version of which is needed at one step of the proof of FLT.
After a lot of headaches I managed to convert my #GPG key to a #SSH private key and claim the #FLT airdrop.
Had to write a custom tool to convert the keys since they messed up the verification process and I couldn't find anything for ed25519 keys.
https://github.com/pinpox/pgp2ssh
I (now) find it quite funny that a company that calls themselfs "crypto" messes up asymetric encryption and excludes users using modern key standards 
Pleasure to work with you @felschr
https://www.shadertoy.com/view/cd3fWs
Here's a GLSL script hosted in Shadertoy that extends the concept of Steiner chains from simple circles to Generalized Circles, and renders them in real-time with user controls.
The code permits specification of any containing circle or half-plane you like, specify the center of the inner circle (or half-plane) around which the chain circles are arranged, and specify the contact angle of the chain itself, with reference to either the containing or inner circle.
This demo chooses the configuration of the containing circle, the user controls the center of the inner circle with the mouse.
Click-and-drag the mouse to move the center of the white circle; use the arrow keys to fix the orientation of the key chain circle (the dark red one) to a particular direction. Various config parameters start around line 90.
I'd love feedback and suggestions, let me know!
Under the hood it's all based on finding just the right FLT to map a trivially-constructed concentric chain of length n within the unit circle to the desired config.
Hardcore fans may recall that a pre-rendered version of this was my first ever post : https://mathstodon.xyz/@KleinianArborist/110674924302552811
@bugaevc Firewalls are about granularity of control, separation of concerns and the strength of heterogeneous solutions.
A software firewall does nothing when everything goes right, but could save your date when you get infected by ransomware and the virus can't connect out because your firewall says, "I don't know you."
[I have truly marvellous demonstrations of the other two reasons which this toot is too small to contain. #left_to_the_reader #FLT]
