C.B. Aberlé

Corinthia Beatrix Aberlé. Aspiring logician. PhD student in CS/Pure and Applied Logic at Carnegie Mellon University. she/her

website: https://cbaberle.com
blog: https://hyrax.cbaberle.com

Last Notes

2026-09-09 00:46:56 UTC

one nice thing about working on more niche problems with less public attention around them is that there's fewer vultures circling them.

2026-03-31 17:27:24 UTC

- reply

Having spent several years in the trenches of formalized mathematics by now, I'm actually more sympathetic @npub1nf4…nqe4 's line of thinking than I used to be, but I think there's nothing about formalized mathematics *per se* that forces this to be the case.
The way I've come to use proof assistants/etc. over the years actually, counterintuitively, ends up making math more "empirical," in a way. My informal proofs and ideas become "hypotheses" I can "test" by attempting to find a formalism and suitable abstractions that make them checkable by a computer. And like any good scientific experiment, this quickly becomes an iterative process—take some informal ideas, attempt to formalize them, get some data back about what ends up being difficult, refine the ideas, repeat until a satisfactory equilibrium is found. And this process itself can lead to a lot of "a ha" moments and "radical" new ideas, itself.
As already noted, however, this process carries the risk of railroading one's thoughts into those ways of thinking that are more easily formalized in a particular system. But imo this is a failure of that particular system to be sufficiently syntactically/semantically flexible, and not of formalism/interactive theorem proving in general.
The future I hope for, and which I am actively building toward, is one in which we have general systems for defining, simulating, and verifiably translating between different logical/formal systems, so that if someone has a new mathematical idea they want to try out it's easy to get up and running with a system for testing it and relating it to other frameworks.
@npub18a6…szuj @npub1vlc…mzqq @npub14a5…9fse [@JacquesC2](https://types.pl/@JacquesC2 ) [@pigworker](https://types.pl/@pigworker ) @npub1vzx…ncd7

2026-03-23 00:55:44 UTC

- reply

Fixed! Thanks, John!

2026-03-23 00:34:05 UTC

New blog post up on my website: How Algebraic is Algebraic Geometry? https://cbaberle.com/Blog/How+Algebraic+is+Algebraic+Geometry%3F
This post was the result of me trying to wrap my head around some of the central concepts of modern algebraic geometry and its generalizations from the perspective of someone more at home in type theory, category theory, programming languages, etc. In particular, I've been watching much of the recent work on "synthetic algebraic geometry" with some interest, and also have had a passing interest in the programme of trying to develop geometry over "the field with one element," due to my longstanding interest in the Riemann Hypothesis and the various research programmes it has spawned. If any of that sounds interesting to you, then I hope that this blog post can be as illuminating for you to read as it was for me to write :)
Tagging a few people who I think might find this interesting and/or whose writings on these and related topics have been stimulating to my thinking on this subject: @npub1jxf…0dxv @npub1nf4…nqe4 @npub1eng…zqfn @npub17yd…03sq
Comments, feedback, and criticism are much welcomed! In particular, please do let me know if I got anything wrong! Like I said, I'm very much an outsider to these subjects trying to understand them better for myself.

2026-02-10 22:05:19 UTC

- reply

yes, absolutely! :)

2026-02-10 00:58:30 UTC

- reply

thank you so much, John!

2026-02-09 16:52:50 UTC

First up on the list of recent additions to my website: something that's a bit different from my usual work on type theory, etc., but that's also very near and dear to my heart—The Music of the Primes ( https://cbaberle.com/Blog/The+Music+of+the+Primes ) a blog post exploring the fascinating connections between musical tuning, the Riemann Zeta function, and linear algebra over the integers!
Some others on this server (e.g. @npub1nf4…nqe4 ) have touched on these topics before, but they've been a pet obsession of mine for the last several years, owing to my joint musical and mathematical background, and this blog post is a fairly comprehensive write up of my findings! Check it out if you're interested!

2025-03-08 01:14:28 UTC

- reply

"We train young men to drop fire on people, but their commanders won't allow them to write 'fuck' on their airplanes because it's obscene!"—Walter Kurtz (Marlon Brando), Apocalypse Now
also, as others have already said, thank you so much for talking about this 🏳️‍⚧️❤️

2025-01-20 20:23:51 UTC

- reply

https://media.mathstodon.xyz/media_attachments/files/113/862/547/372/284/063/original/0631ed21d04d7d43.jpeg