theHigherGeometer

rimcræftiga |
bespoke constructions in categorified geometry since 2010 |
dude

Public Key

npub1p2q4c7sn2jgtj3w7g9syy5zjldxd8e5ruknf99g8y636ls8vx8esq5c0lr

NIP-05 Address

Profile Code

nprofile1qqsq4q2u0gf4fy9egh0yzczz2pf0knxnu6p7tf5jj5rjdga0crkrrucpz4mhxue69uhhyetvv9ujuerfw36x7tnsw43qz9thwden5te0wfjkccte9ekk7um5wgh8qatzlgv40s

Publishing to

relay.ditto.pub

relay.mostr.pub

Author Public Key

npub1p2q4c7sn2jgtj3w7g9syy5zjldxd8e5ruknf99g8y636ls8vx8esq5c0lr

Show more details

Last Notes

2026-02-13 03:27:15 GMT

- reply

@nprofile…72nl From WP:
"The first known use is in a 1957 syndicated newspaper article about US Army mathematicians and their work with early computers,[3] in which an Army Specialist named William D. Mellin explained that computers cannot think for themselves, and that "sloppily programmed" inputs inevitably lead to incorrect outputs."
https://en.wikipedia.org/wiki/Garbage_in,_garbage_out

2026-02-10 01:26:52 GMT

- reply

@nprofile…7md8 That recording booth looks like the one that @nprofile…fh5u used, IIRC!

2026-02-10 01:24:42 GMT

I wish that some internet trolls were this level of "barely literate" when complaining about how certain authors' works are adapted.
Or for that matter, billionaires who like cool invented names and steal them for their companies, ignoring the context, the ethos, and the themes....

2026-02-10 00:56:52 GMT

Fun discussion involving @nprofile…u3x7 about Lean security vulnerabilities (more at link)
https://leanprover.zulipchat.com/#narrow/channel/423402-PrimeNumberTheorem.2B/topic/LeanCert.20for.20numerical.20log.20bounds.20.28re.3A.20PNT.23892.2C.20PNT.23914.29/near/572854830
https://media.mathstodon.xyz/media_attachments/files/116/043/595/822/310/616/original/8a2f7aa9bed40524.png

2026-02-09 14:16:03 GMT

- reply

It's a bad pun

2026-02-09 09:15:07 GMT

- reply

@nprofile…4257 Oh, cool, thanks!

2026-02-09 07:28:37 GMT

- reply

@nprofile…4257 Sure. Obviously people aren't solving in anything like just 20 moves, but I can certainly imagine that perhaps the scramble happened to produce a state such that his preferred algorithm resulted in a rather-shorter-than-average move sequence.

2026-02-09 04:09:21 GMT

German captain's favourite film about Italian geography? (3,4)

2026-02-09 02:08:32 GMT

- reply

@nprofile…4257 I guess I can watch this video later to see the details: https://www.youtube.com/watch?v=il3ElZEY-qw

2026-02-08 23:19:41 GMT

- reply

@nprofile…4257 How much of this is down to a lucky scramble? In other words, how many moves did it take? (perhaps this is answered in the video, sorry)

2026-02-08 09:44:07 GMT

- reply

@nprofile…lfhd @nprofile…gpz3 Sure, but you have to establish the required radius of convergence to know that π is something that be extracted. I was interested in an elementary-as-possible approach.
[Lárusson's short lecture notes on real analysis book (which I once formally reviewed) does it by establishing that the zero-set of \(\sin\), defined by a power series is a discrete additive subgroup of the reals, but this is not early in the book!]

2026-02-08 03:44:41 GMT

- reply

@nprofile…gpz3 I can't remember!

2026-02-07 12:08:45 GMT

Having taught first-year calculus, including things like geometrically deriving \(\tfrac{d}{dx}\sin(x)\), and estimates on errors from Taylor polynomials, and also liking the kind of foundational subtleties in analysis that can be broken down to understandable chunks, I agree that Archimedes' argument involving more than one round of estimates (post 2/3 in the below mentions \(256/153 < \sqrt{3} < 151/78\) as going into the process of calculating the bounds for π. Once my colleague Raymond Vozzo and I tried to work out what was the clearest/simplest way to completely rigorously define π or 𝑒, in the sense of analysis. It's not trivial!

2026-02-05 10:01:29 GMT

- reply

@nprofile…4hp5 I've been keeping half an eye on what he has been doing with his collaborators over the past decade or so, it's definitely fun to watch. Having a sketch of Connes' current ideas at the level of 19th century tech (sweeping a few things under the rug that got proved in the early 20th century) was a fascinating exercise. It reminds me of when arithmetic geometers give talks that give an on-ramp to a key modern conjecture in terms of some really concrete classical problem, like the congruent number problem leading to elliptic curves and then Tunnell's theorem, which is conditional on the BS-D conjecture.

2026-02-05 06:14:51 GMT

New from Alain Connes. His "Letter to Riemann" is fun.
https://arxiv.org/abs/2602.04022
He is honest about the fact we cannot prove the RH, and that it's not clear if his preferred approach will be the way, but also:
"Our discovery of a large class
of functions directly related to the Weil quadratic form and with zeros provably on the critical line, combined with the extraordinary numerical evidence linking truncated Euler products to the actual zeros of zeta, suggests that Riemann’s original insights may contain more power than previously realized. The accuracy achieved using only primes less than 13—with errors as small as \(2.6 \times 10^{-55}\)—cannot be dismissed as coincidence"
Apparent numerical coincidences in number theory like this at very minimum demand an explanation.

2026-02-02 06:01:00 GMT

- reply

@nprofile…hh7n I can't say I'm needing to temper my excitement.

2026-02-02 03:39:33 GMT

I heard a merger fact today that requires me to actively make myself calm down.
I don't think I can share it publicly, so I won't be.

2026-02-01 10:50:37 GMT

- reply

@nprofile…dn5h Miss R has the same one! Her name here is Mimi, after a grey cat in an old kids book we have read.

2026-01-29 22:23:19 GMT

- reply

@nprofile…lfhd On the sentence "Cet exposé fait suite à celui d’il y a deux ans (25 janvier 2024)," the link on celui is broken!
https://webusers.imj-prg.fr/~antoine.chambert-loir/exposes/tb-20240125.pdf

2026-01-29 05:12:15 GMT

- reply

@nprofile…hh7n It's presumably coming out of this published work https://doi.org/10.1093/logcom/exae034. Here's what seems to be the (very brief) paper underlying the talk: https://arxiv.org/abs/2512.12892

2026-01-29 05:11:08 GMT

- reply

@nprofile…hh7n It's presumably coming out of this published work https://doi.org/10.1093/logcom/exae034. Here's what seems to be the paper underlying the talk: https://arxiv.org/abs/2512.12892

2026-01-29 03:26:11 GMT

From Sergei Artemov, talking next at the the NYC CT seminar. The best bit is in the last paragraph.
-----
Abstract: Non-compact proofs are used in mathematics but overlooked in the analysis of (un)provability of consistency. We focus on arithmetical proofs of universal statements (*) "for any natural number n, F(n)." A proof of (*) is compact if all proofs of F(n)'s for n=0,1,2,... fit into some finitely axiomatized fragment of Peano Arithmetic PA. An example of non-compact reasoning is the standard proof of Mostowski's 1952 reflexivity theorem: PA proves the consistency of its finite fragments.
It turns out that Gödel's Second Incompleteness Theorem, G2, prohibits compact proofs but does not rule out non-compact proofs of PA-consistency formalizable in PA. This explains why and how the recent proofs of PA-consistency in PA work: they essentially formalize in PA the explicit version of Mostowski's non-compact proof and use Gödelian provable explicit reflection to rid redundant provability operators.
These findings yield a new foundational reading of G2: "the consistency of PA is not provable within a finite fragment of PA," complemented with the positive message: "the consistency of PA is provable within the whole PA." This perspective suggests that Gödel's theorem does not represent a failure of the system to "know" its own consistency, but rather a structural limit on how that knowledge can be packaged into a single finite string.

2026-01-28 23:01:26 GMT

- reply

@nprofile…xuzd Thanks to this post, I looked and discovered the macOS Mail app can be configured to the layout I remember from the mid-00s, as you described in 1.

2026-01-28 10:16:34 GMT

- reply

@nprofile…fws0 Thanks :-) now that things are in full swing, are participants likely to make their slides available on the conference site?

2026-01-28 10:02:19 GMT

- reply

@nprofile…fws0 How's this morning's talk on Chevalley?
I ask because Serre once answered a question of mine, and noted of him "c'était le plus puriste des membres de Bourbaki."

2026-01-28 01:57:20 GMT

- reply

@nprofile…7jv6 Well done, authors.

2026-01-27 23:54:47 GMT

Oops.
https://media.mathstodon.xyz/media_attachments/files/115/969/753/170/360/914/original/696bcdcb5d494db0.png

2026-01-27 20:36:32 GMT

- reply

@nprofile…udvu I agree it made the expert testimony of the engineers nigh impossible to ignore, so it wasn't for nothing.

2026-01-27 20:10:56 GMT

Amazing, no need for a stunt by a certain physicist to magically discover and reveal why...
https://www.abc.net.au/news/science/2026-01-28/space-shuttle-challenger-disaster-nasa-explosion-video-engineers/106162902

2026-01-27 01:38:49 GMT

- reply

@nprofile…wncd @nprofile…4hp5 Just commenting so I can listen in

2026-01-26 09:15:33 GMT

- reply

I fear "Congregati ex toto orbe mathematici" might ring a little hollow this year...

2026-01-26 08:37:31 GMT

- reply

@nprofile…7jv6 Well, it has been shown that an online ICM can be done, and with less lead-up time than if a similar decision were made this month.

2026-01-26 08:24:00 GMT

I say the following reluctantly, since I leave the online discussion of politics to others better versed and placed to do so. My voice is not that strong, and does not count for much, but I do wish the IMU would publicly address what is going to happen to the ICM this year. The leadership would, I hope, either make a hard call sooner rather than later to shift venues, or explain why not. Or, at absolute minimum, let everyone know if there are ongoing discussions the outcomes of which will be announced in due course. I cannot imagine such discussions aren't happening.
#ICM2026

2026-01-25 19:35:33 GMT

- reply

@nprofile…l3hr Tolkien scholarship still differentiates between the two, since they represent distinct drafting phases. The same document can even flip from typescript to manuscript mid-way! Or you can have a manuscript that is then (possibly years later) copied as an amanuensis typescript, then hand edited and then with additional manuscript pages or riders. The specific typewriter and/or pen used gives (coarse) info about dating!

2026-01-21 03:26:21 GMT

- reply

@nprofile…4hp5 No, he's opening up his book by description of natural numbers and then different kinds of numbers that arise in solving problems (squares, 'roots' etc)
https://archive.org/details/algebraofmohamme00khuwuoft/page/5/mode/1up

2026-01-21 03:08:21 GMT

"When I consider what people generally want in calculating, I found that it always is a number."
—Abu Ja'far Muhammad ibn Musa Al-Khwarizmi, https://en.wikipedia.org/wiki/Al-Jabr ca.820
TIL this is the opening sentence of the book proper (after the author's preface).

2026-01-20 23:29:35 GMT

- reply

@nprofile…cytr I guess ?tela aranea means 'spider's web'? (Latin, no?)

2026-01-20 09:51:43 GMT

- reply

@nprofile…wkcu Thanks. I'm interested in a very specific item: the use of = instead of a symbol for isomorphism (≃ or ≅ etc), which someone once suggested to me might have been a shortcut (before widespread computer typesetting, perhaps driven by typewriter usage) that people at the time could have used with full knowledge that it was really an isomorphism.

2026-01-20 06:54:46 GMT

- reply

@nprofile…4hp5 Good thing I'm keeping myself under that limit already....

2026-01-20 05:37:13 GMT

"I’ve decided to push back on the pressure to publish by making a rule for myself: I will no longer publish more than seven papers per year. I’ve published a median of 15 papers a year for the past five years, so that means I will have to halve my output. "
🤯
https://doi.org/10.1038/d41586-025-04061-w
(From a member of the research committee of Australia's NHMRC, the main medical research funding body here)

2026-01-20 02:58:09 GMT

- reply

@nprofile…lfhd Awesome! Bravo

2026-01-20 02:57:10 GMT

- reply

@nprofile…wkcu I wonder if there is an analogue of this for mid-century *French* mathematical printing.

2026-01-20 02:15:53 GMT

- reply

@nprofile…fws0 Hmm, looking at a different conference on the same platform, I see that it has a similar setup, but the abstracts are linked from the schedule in that one. I don't want to make more work for anyone, but I hope that perhaps the abstracts will land at some point (not to mention slides etc after the fact).

2026-01-20 02:11:40 GMT

@nprofile…fws0 sorry to be a pain, but the link that says 'abstracts' on https://conferences.cirm-math.fr/3523.html points instead to a differently-formatted version of the schedule instead. Is this intentional?

2026-01-18 03:48:19 GMT

"while that gives you science, it doesn't give you press releases."
Precisely

2026-01-17 23:30:08 GMT

- reply

@nprofile…u3x7 Since trying an AI system on solving mathematics problems is essentially experimental science, one might reasonably demand https://en.wikipedia.org/wiki/Preregistration_(science) as a standard for the field, like in other experimental sciences

2026-01-16 06:01:58 GMT

If you see a paper on the arXiv claiming a proof that Reinhardt cardinals are inconsistent with ZF, note that the author already claimed this in a prior arXiv preprint and retracted it. And also claimed a proof of P ≠ NP.
I cannot make an informed judgement about the new paper, but I would await experts' assessment before leaping to conclusions.

2026-01-16 00:21:24 GMT

https://www.abc.net.au/news/2026-01-16/qld-woman-wakes-to-find-python-on-top-of-her-snake-season/106233916
#straya

2026-01-15 23:30:41 GMT

- reply

And here's a write-up on @nprofile…cu8d 's blog
https://davidkbutler.xyz/2016/09/20/sqwigles/

2026-01-15 21:57:07 GMT

From @nprofile…cu8d, nearly 9 years ago.
https://www.youtube.com/watch?v=u3v_7G5D5xI

2026-01-15 06:35:16 GMT

> Stephen explained this to me by saying that you cannot make jokes about failure in the States. It’s like cancer, it just isn’t funny at any level. In England, though, for some reason it’s the thing we love most.
This explains a lot, including LinkedIn.

2026-01-14 23:06:28 GMT

- reply

@nprofile…rk9k I like the idea of trying novel visualisations here, I might have a think and give you some feedback

2026-01-14 08:24:16 GMT

- reply

@nprofile…l3hr I saw 'theory type theory' recently in a block of text and it looked like a typo!
TIL a new thing,
Two references I found
https://www.carmin.tv/en/video/towards-synthetic-locale-theory
https://topos.institute/blog/2025-07-13-liberating-synthetic-quasi-coherence-from-forcing/

2026-01-13 23:31:38 GMT

Interval arithmetic implemented in Lean, to get verified numerical computation:
https://github.com/alerad/leanbound

2026-01-13 21:47:37 GMT

There's a multi-site drama going on involving BSky and meta.MO right now. I'm not going to add to it here, and don't wish to spread the muck, but anyone who is seeing it please be aware the board and the mods are aware and discussing.

2026-01-13 21:45:58 GMT

- reply

@nprofile…hh7n Oh, cool, thanks! I recognised some editor names, so my originally drafted comment was much softened to the above.
@nprofile…sqfw

2026-01-13 11:29:35 GMT

A great report of an experiment by Asaf Karagila with LLMs (not just ChatGPT), asking them about his own (public) work. Spoiler: results are very patchy at absolute best
https://karagila.org/2026/chatgpt/

2026-01-13 07:58:16 GMT

I don't think this old question is quite resolved
https://mathoverflow.net/questions/281660/stacks-algebraic-over-a-given-stack

2026-01-13 07:08:15 GMT

- reply

@nprofile…sqfw The publisher seems a little niche (speaking generously) but the paper seems serious.

2026-01-13 04:39:44 GMT

The following article claims that the logic in Kant's "Critique of Pure Reason" is _geometric logic_, and not some incomplete, too-weak system as had apparently been the consensus view.
Achourioti, T., & van Lambalgen, M. (2017). "Kant's logic revisited". The IfCoLog Journal of Logics and their Applications, 4(4), 845-865.
https://pure.uva.nl/ws/files/26494036/Kants_logic_revisited.pdf

2026-01-13 04:38:56 GMT

The following article claims that the logic in Kant's "Critique of Pure Reason" is _geometric logic_, and not some incomplete, too-weak system as had apparently been the consensus view.
Achourioti, T., & van Lambalgen, M. (2017). "Kant's logic revisited".
The IfCoLog Journal of
Logics and their Applications,
4(4), 845-865.
http://www.collegepublications.co.uk/ifcolog/?00013
(https://pure.uva.nl/ws/files/26494036/Kants_logic_revisited.pdf)

2026-01-12 23:01:45 GMT

Last night I had a Japanese-themed beef-topped pizza. It had pickled ginger, sesame seeds, Kewpie mayonnaise etc. It was really nice!

2026-01-12 22:59:15 GMT

- reply

@nprofile…7jv6 oh, that's interesting. It perhaps give a psychological release valve to mark something on the page rather than do nothing and feel guilty about it.
@nprofile…t6k2

2026-01-12 22:59:06 GMT

- reply

@nprofile…7jv6 oh, that's interesting. It perhaps give a psychological release valve to mark something on the page rather than do nothing and feel guilty about i.
@nprofile…t6k2

2026-01-12 11:28:36 GMT

- reply

@nprofile…lfhd The slides link on your site is broken! https://webusers.imj-prg.fr/~antoine.chambert-loir/exposes/20260111-cpp2026

2026-01-12 10:01:25 GMT

Very nice looking proof!

2026-01-11 06:20:06 GMT

- reply

@nprofile…j36t Fair enough.

2026-01-11 06:12:17 GMT

- reply

@nprofile…g0zc And of course: https://www.speedrun.com/upc people are still setting world-record times

2026-01-11 06:08:52 GMT

- reply

@nprofile…g0zc The numbers of pages on the Wiki are small now, but just you wait!

2026-01-11 06:05:03 GMT

- reply

@nprofile…j36t Do they not have an option of giving your talk remotely? Or even just a prerecorded talk? In today's world this seems an absolute no-brainer, since people might not travel for all kinds of reasons: parenting, caring responsibilities, environmental concerns, visas being denied on 'curious' grounds etc.

2026-01-10 23:15:29 GMT

- reply

Here's the original paper: https://arxiv.org/abs/dg-ga/9407015

2026-01-10 08:28:36 GMT

https://doi.org/10.1112/jlms.70374
Not every day someone's paper gets a review 30 years later by a leading figure in the same (top-notch) journal. Michael invented the main definition in his now-classic paper while waiting for Brylinski's then-recent book on gerbes to be shipped to Australia, based on the tiny blurb in a publisher's ad for it.

2026-01-10 06:26:45 GMT

- reply

@nprofile…r0xq not a problem, it made me check

2026-01-10 06:02:22 GMT

- reply

@nprofile…r0xq no, that is mentioned higher up:
"A correction is needed to the Section on the Phragmen-Brouwer Property and the details are in Brouwer correction, 6 pages. arXiv: 0948151"

2026-01-09 06:42:09 GMT

A very useful compilation of hypotheticaledits to the 1977 Silmarillion that, among others, lists errors pointed out by Christopher Tolkien and what they should have been instead.
https://web.archive.org/web/20240529041103/http://tasarinan.atwebpages.com/silmap.html

2026-01-08 09:26:18 GMT

- reply

@nprofile…sqfw the point was the enormity of the paper. And it's one of four in the series. Paper 3 is comparatively short (it's on the arXiv) if not short in absolute terms, but paper 4 isn't out yet. Also, a subset of the authors have a separate application paper that's 100 pages long...

2026-01-08 08:25:29 GMT

- reply

@nprofile…sqfw I can't do better than the intro, which I only skimmed the very start of...

2026-01-08 05:21:01 GMT

- reply

@nprofile…4eh5 Oh, really? That's pretty annoying.

2026-01-08 05:20:39 GMT

- reply

"'canonically' splits" ok then.... 🙄
@nprofile…pm2x how does this main claim in an Acta paper make you feel?
https://media.mathstodon.xyz/media_attachments/files/115/857/782/657/358/720/original/5002d7e73a636743.png

2026-01-08 05:03:55 GMT

- reply

Cool, actual scenes...
https://www.youtube.com/watch?v=Md5a_EavdzE
https://www.youtube.com/watch?v=vLV39w1W1Y0

2026-01-08 04:53:05 GMT

- reply

You can see a little sample in this trailer https://www.youtube.com/watch?v=LcPgRymHCos If they pulled in parts of the story from the whole of the manga that would get pretty mind-bending. The issues of staging things like the god-warrior and the ohmu (done as puppetry it seems, very nice) are minimal compared to the inner psychological journey Nausicaä goes on deeper into the story than what the animated film version covered.

2026-01-08 04:49:16 GMT

https://web.archive.org/web/20200828172141/https://www.polygon.com/2020/8/28/21405363/nausicaa-of-the-valley-of-the-wind-play-kabuki-miyazkai-watch-streaming
!!!! A stage adaptation of the manga of Nausicaä!

2026-01-08 01:09:53 GMT

- reply

Paper I is 269 pages.... https://doi.org/10.1007/s00029-022-00758-2

2026-01-08 01:07:24 GMT

Nine authors and ~250 pages (! note author order). This paper takes up the whole issue of Acta, and took four or so years to get accepted, it seems...
Baptiste Calmès, Yonatan Harpaz, Markus Land, Denis Nardin, Wolfgang Steimle, Emanuele Dotto, Fabian Hebestreit, Kristian Moi, Thomas Nikolaus, "Hermitian K-theory for stable \(\infty\)-categories II: Cobordism categories and additivity" Acta Mathematica
Volume 235 (2025) Number 2 pp. 149-400 https://doi.org/10.4310/ACTA.2025.n235.n2.a1 https://arxiv.org/abs/2009.07224

2026-01-08 00:35:39 GMT

- reply

I have read Beckett for example, and Ionesco, and enjoyed them at the time, so either my tastes have shifted, or it's just not that similar.

2026-01-07 23:15:54 GMT

- reply

@nprofile…t6k2 "January 2020
A recent errata list compiled with Taras Kolomatski (20-20) MoreT&G errata (RB & TK"
with broken link
https://groupoids.org.uk/pdffiles/topgpdserratta20_20.pdf

2026-01-07 23:11:52 GMT

- reply

@nprofile…t6k2 the pdf file was compiled in 2020 by someone I guess was a student at the time....

2026-01-07 23:10:38 GMT

Tom Stoppard's 'Rosencrantz and Guildenstern are Dead'. I saw the film adaptation nearly two decades ago and enjoyed it, more than reading the play. I think I would get more mileage out of seeing it performed. At times what was presumably the fast and witty wordplay seemed tedious. There were a few moments I felt were fun, but this feels more like something you'd study academically for maximum benefit. My copy was second-hand and had someone's annotations which was kinda interesting.
#Read2026
https://media.mathstodon.xyz/media_attachments/files/115/856/043/721/811/366/original/24736f45c6668b07.jpg

2026-01-07 22:57:37 GMT

Oh dear: an erratum file for Ronnie Brown's book 'Topology and Groupoids' at the end of this page is missing (no Wayback Machine capture!)
https://groupoids.org.uk/topologygpdserrata.html
does anyone have a copy, or know how to get in touch with Taras Kolomatski to try to get one?

2026-01-07 11:19:27 GMT

- reply

@nprofile…7jv6 you keep a list and keep updating it https://shelah.logic.at/paper-list/

2026-01-07 05:18:45 GMT

- reply

The first proof in the paper says to pick four cardinal parameters to be the specific values \(\aleph_6,\aleph_5,\aleph_2\) and \(\aleph_0\) and then apply a more complex main theorem.
I mean, this is the guy who proved
\[2^{\aleph_\omega} < \aleph_{\omega_4}\] which never ceases to boggle my mind.

2026-01-07 05:10:44 GMT

"This is publication number 1258 on Saharon Shelah’s list"
Of course it is 🫠
https://arxiv.org/abs/2601.02923

2026-01-07 04:31:06 GMT

Description of the archives, not online access. But I'd be interesting ultimately in seeing 'HC 3/7 - HC 3/11 Séminaire de mathématiques de l'ENS', because it overlaps with the first years of Bourbaki.
For example, I'd love to see this one:
- Exposé de Charles Ehresmann, « Topologie combinatoire. - les groupes d'homologie », 18 novembre 1935, 3 exemplaires. (from HC 4/1/2 - HC 4/3 Troisième année du séminaire de mathématiques de l'ENS : topologie)
and of course 'HC 5/9 - HC 20/4 Bourbaki'
And there's La Tribu up to number 177 (in 2006!) Still digging through to see if there's anything else I like the look of.

2026-01-06 23:54:55 GMT

- reply

@nprofile…2p65 I didn't check!

2026-01-06 11:34:24 GMT

Some non-set theoretic philosophy in there would be nice, yes

2026-01-06 09:55:32 GMT

https://github.com/KonjacSource/Russell-paradox-in-TT 👈 formalisation here

2026-01-06 09:51:22 GMT

This should be easily encodable in say Agda, if sound.

2026-01-05 14:43:34 GMT

- reply

And home at 1am 😕 😴

2026-01-05 08:46:01 GMT

Big day of driving. >450km till home and its 7:45 local time (will gain half an hour when we cross the state border, but that doesn't help much!)

2026-01-04 00:32:44 GMT

- reply

@nprofile…exh5 ooooh!