#aboutlogic — Public Fediverse posts

After listening to the latest #aboutlogic episode on synthetic mathematics I was wondering if anybody actually developed simple synthetic geometry in #Agda.

In particular, I wonder what a synthetic proof of the pythagorean theorem would look like. There are many nice visual proofs, but they seem hard to implement in a proof assistant.

I met Urs a couple of years ago when he was in Bonn. He is a great teacher and he made the history of the standard model come alive for me, especially illuminating the interaction between physicists where all I had known were singular biographies! He also made me learn about cohomology theory! A few weeks ago I looked him up on Youtube and found this recent reccording:

Urs Schreiber: "The $1 Million Puzzle: Hadrons and Quantum Computers", second draft recording
https://www.youtube.com/watch?v=1jOQut1eOI0

It's fast a fast paced talk touching boundaries of known particle physics, topological quantum computing, and ultimately, making a point demanding topological methods to get at new physics! He's not here to promote his final answer, but he has clearly always been passionate about homotopy theory. The idea is that HoTT (Homotopy Type Theory) may be relevant to particle physics, emphasizing that that brings computation into the picture! I really like his style, the sun coming from behind makes for quite some atmosphere.

There's also this fresh interviewby #aboutlogic, I haven't seen yet:

aboutlogic #12: Urs Schreiber – Quantum (Physics, Computing), Topos & Homotopy Theory
https://www.youtube.com/watch?v=V7749J5-lho

I haven't seen this announced here: My colleague Thorsten Altenkirch launched a new podcast #aboutlogic together with cohost @DenizPhiMa – I enjoyed the first three episodes with Thorsten, Deniz, and @xenaproject, respectively. Find it in your podcast app (RSS https://aboutlogic.podigee.io/feed/mp3) or watch on YouTube (https://www.youtube.com/@aboutlogic). #logic #mathematics #philosophy #computerscience