About Logic - Theorem Proving, Constructive Mathematics and Type Theory

It's going to be a regular podcast with Thorsten Altenkirch and Deniz Sarikaya, and this is episode one:

19:51 On Synthetic Homotopy Theory. See Synthetic Homotopy Theory with HoTT/UF.

See https://github.com/agda/agda.

See also FOMUS: Foundations of Mathematics: Univalent Foundations and Set Theory - What are Suitable Criteria for the Foundations of Mathematics?, Emily Riehl on Univalent Foundations and Another Excellent Talk on HoTT by Steve Awodey. 

And another episode:

22:02 On the use of computers in theorem proving. You can get a situation where a hugely complex lemma is formally proven and turns out to be useful in proving a perfectly intelligible theorem, but the proof is unintelligible because it relies on this incomprehensible lemma. 

And another:

My comment:

10:50 His job was done?! What about reproducibility? If you formally prove some theorem in one system, and a hundred other people run the same code through the same system, just on different computers, is that really enough? Don't you need to formally describe the Lean prover in such a way that anyone else can write their own theorem prover and run the same proofs? So the next step would be to formally specify a specification language and use that to formally describe the Lean type system, then you need to formally specify a language for writing expressions and another for specifying type checkers and then people can translate these axiom systems and type checkers into actual running code on whatever hardware they want. Until you do that you aren't really proving theorems, you're just playing around with a computer program. The discussion at 24:27 on axioms is relevant here. [See also Thorsten's comments about constructivism at 21:43 in the first discussion.] Also the discussion at 35:58 on definitions. You don't need to go as far as the reals to see the issue. Even the implementation of pairing in set theory "shows through". See the 1999 paper Final Coalgebras as Greatest Fixed Points in ZF Set Theory by Lawrence C. Paulson.

Subscribe to About Logic. 

Comments

Post a Comment

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Image
A derivative is linearisation, and differential calculus is essentially linear algebra, ...  See  Freya Holmér - Why Can't You Multiply Vectors?  and  Freya Holmér on Continuity of Splines . See also the MIT OCW page:  Matrix Calculus For Machine Learning And Beyond  (Alan Edelman, Steven G. Johnson) Subscribe to The Julia Programming Language . Alan Edelman talking about expressing mathematics as computer code. The idea is that you can use computer languages to communicate mathematical ideas precisely to other people. See my comments about functional programming languages here:  https://prooftoys.org/ian-grant/hm/ Subscribe to TEDx Talks .
Read more

Hitachi HD44780U LCD Display Fonts

Image
I finally got the bit-mapped fonts from the Hitachi "1602" display :  Here's some JavaScript: const HD44780U01ASCII=[ [],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[], [],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ], [4, 4, 4, 4, 0, 0, 4, 0, 0, 0, ], [10, 10, 10, 0, 0, 0, 0, 0, 0, 0, ], [10, 10, 31, 10, 31, 10, 10, 0, 0, 0, ], [4, 15, 20, 14, 5, 30, 4, 0, 0, 0, ], [24, 25, 2, 4, 8, 19, 3, 0, 0, 0, ], [12, 18, 20, 8, 21, 18, 13, 0, 0, 0, ], [12, 4, 8, 0, 0, 0, 0, 0, 0, 0, ], [2, 4, 8, 8, 8, 4, 2, 0, 0, 0, ], [8, 4, 2, 2, 2, 4, 8, 0, 0, 0, ], [0, 4, 21, 14, 21, 4, 0, 0, 0, 0, ], [0, 4, 4, 31, 4, 4, 0, 0, 0, 0, ], [0, 0, 0, 0, 12, 4, 8, 0, 0, 0, ], [0, 0, 0, 31, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 12, 12, 0, 0, 0, ], [0, 1, 2, 4, 8, 16, 0, 0, 0, 0, ], [14, 17, 19, 21, 25, 17, 14, 0, 0, 0, ], [4, 12, 4, 4, 4, 4, 14, 0, 0, 0, ], [14, 17, 1, 2, 4, 8, 31, 0, 0, 0, ], [31, 2, 4, 2, 1, 17, 14, 0, 0, 0, ], [2, 6, 10, 18, 31, 2, 2, 0, 0,...
Read more

Using Pipewire to Make A Music Synthesizer

Image
Illustration from Project Gutenberg's The Tenniel Illustrations for Carroll's Alice in Wonderland by Sir John Tenniel. Thinking about the linux desktop audio problem: I'm not the only one who finds this weird: https://t.co/b2BZMiak07 — eternal Doorman (@IanANGrant66) May 17, 2025  I noticed that if you change the volume using the Gnome volume keys it changes it in jumps. Usually you don't notice, but if you play a pure sine tone then you can easily hear the distortion. If you want to play with pipewire from C on Ubuntu 24.04 then it's really easy. The pipewire tutorials and examples can be compiled and run if you just first install the pipewire-0.3-dev package with sudo apt install libpipewire-0.3-dev But the API is sooo far away from pluggable, typed streams that I find it quite depressing. Is it because nobody understands the necessary type system . See  Programming Channel Processes and Alice's Adventures In The Wonderland Wide Web . [Update: y...
Read more