Andrej Bauer / is on Nostr

"63eba2efb7559deccabb6e7de09da418ddd9356e44aad43f4dcc5bb005982897641dc1aa88954799854805dd7ba0c2e0736a895c335598205261399ce7d8b10e"

Last Notes

2025-04-02 08:48:47

A revised version of the “The countable reals“ paper is available. We threw out the faulty proof of "all maps are continuous", which therefore been relegated to an open problem.
The topos is very good at defying proofs that use the recursion theorem from computability. This is not a surprise, as the topos was constrcuted precisely for the purpose of defiting diagonal arguments.
In realizability LPO (every infinite binary sequence contains 1 or is all 0's) is invalid, which is shown using the recursion theorem. In our topos this doesn't work, but a nice idea of Joe Miller's does, so that's a new result in the revised version. The proof that LPO is invalid uses a principle which we call the "Majority Decision principle". I'll post about it separately.
https://arxiv.org/abs/2404.01256

2025-03-17 19:37:03

- reply

@nprofile…59k6 I seem to remember an interview with the AlphaFold designers in which they said it was important to *not* constrain AlphaFold to only physically realized configurations. The learning process was more successful this way.
It may well be the same with learning math. Incorrect constructions must be permitted, but suitably penalized.

2025-03-16 10:20:51

- reply

@nprofile…6kk0 The payoff for writing a monograph is almost negative these days. The pause in publication of (superficial) research papers can endanger one's career, and I know of such examples. You'll be lucky if you can buy half a car from the proceeds, and the publisher will make sure to make the book inaccessible for those who need it most.

2025-02-26 09:08:56

Daily reminder on how good ChatGPT is. I asked it to show me the diagrams for 𝑓 : 𝑇𝐴 → 𝐴 being an algebra for the monad 𝑇.
https://media.mathstodon.xyz/media_attachments/files/114/069/394/823/459/870/original/aeaba1b5f49a2826.png

2025-02-11 17:03:51

- reply

@nprofile…6kk0 It's almost like the Internet.

2025-02-11 13:12:00

I just noticed that synthetic computability is my go-to idea for birthday presents. My paper on fixed-point theorems was for the Lawvere-Freyd issue of Tbilisi journal https://doi.org/10.1515/tmj-2017-0107, the continuity theorems for Dieter Spreen's issue of Logic & Analysis https://arxiv.org/abs/2307.07830 (why hasn't that been published yet?!), and now with @nprofile…nf5n we're cooking up Turing reductions for Jaap van Oosten's symposium in Amsterdam.
So people, if you want to see more progress in synthetic computability, you'll have to celebrate some birthdays.

2025-02-06 17:51:21

- reply

@nprofile…hvl9 @nprofile…6kk0 Actually, you need only ∀ and ⇒ to state the correct definition of well-foundedness, whereas for no-infinite-descending-chains you first postulate ℕ, and then one night you wake up in cold sweat, realizing that well-foundedness of ℕ is stated using well-foundedness of ℕ.

2024-07-19 07:04:57

- reply

@npub1cec…u8re Isn't he just pointing out that equality on reals is ¬¬-stable but not decidable?

2024-05-25 08:59:38

- reply

@npub1knz…c73p Sending this privately: I understand that you have good intentions, but it comes across a bit dismissive. You make it sound as if it would be just a matter of tring a bit harder to switch to HoTT.