I was asked to give a talk today at our informal type theory seminar in Budapest and chose to present (and hopefully not misrepresent) nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyz4g9497lls2ey4v3rxtld6a8m5rh7meav97tqfhnceyja6wn0lpgng99up (nprofile…99up) and James E. Hanson's paper on making the reals countable in constructive mathematics – although I spent most of the time doing an informal introduction to realizability since the audience was not familiar with it. In case this interests anyone, the slides are here:
https://jean.abou-samra.fr/talks/2025-11-10-countable-reals.pdf
Jean Abou Samra (new account)
npub14p…htzwd
2025-11-10 22:31:07 UTC
Author Public Key
npub14pv6xjcsz2qa6tctew034s5wsj5p2xuh65q86qe6gpegaslstc6qjhtzwdPublished at
2025-11-10 22:31:07 UTCEvent JSON
{
"id": "217876ffee848569833a723762c635a0126e07f078d25db447024faadf319511",
"pubkey": "a859a34b101281dd2f0bcb9f1ac28e84a8151b97d5007d033a40728ec3f05e34",
"created_at": 1762813867,
"kind": 1,
"tags": [
[
"p",
"aa82d4beffe0ac92ac88ccbfb75d3ee83bfb79eb0be581379e3249774e9bfe14",
"wss://relay.ditto.pub/"
],
[
"p",
"406cda1605d9d95b1e39a78327c3891afba2baecd30a02b403c900e6d3f9bb58",
"wss://relay.ditto.pub/"
],
[
"proxy",
"https://mathstodon.xyz/users/jeanas/statuses/115527769596787455",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "I was asked to give a talk today at our informal type theory seminar in Budapest and chose to present (and hopefully not misrepresent) nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyz4g9497lls2ey4v3rxtld6a8m5rh7meav97tqfhnceyja6wn0lpgng99up and James E. Hanson's paper on making the reals countable in constructive mathematics – although I spent most of the time doing an informal introduction to realizability since the audience was not familiar with it. In case this interests anyone, the slides are here:\n\nhttps://jean.abou-samra.fr/talks/2025-11-10-countable-reals.pdf",
"sig": "3d8d0217bae04168ffd8707d783cde9a92c521e5eb32385b7a2c28549389b27a1f776003c1ce2cf449705817c4aad753664b0dd9fafa5cf0ddc7d01f763ac42f"
}