Having spent several years in the trenches of formalized mathematics by now, I'm actually more sympathetic John Carlos Baez (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.
Andrej Bauer (npub18a6…szuj) DougMerritt (log😅 = 💧log😄) (npub1vlc…mzqq) Martin Escardo (npub14a5…9fse) [@JacquesC2](https://types.pl/@JacquesC2 ) [@pigworker](https://types.pl/@pigworker ) Kevin Buzzard (npub1vzx…ncd7)
C.B. Aberlé
npub1s2…5f7ya
2026-03-31 17:27:24 UTC
in reply to nevent1q…phdc
Author Public Key
npub1s28a6qpzcu243guvp3snypltaxxcgfwrcdfv8ngjuanlgdgx4hdqv5f7yaSeen on
wss://relay.momostr.pinkPublished at
2026-03-31 17:27:24 UTCEvent JSON
{
"id": "0d2636fe86fd47cabbb7733e61d859bbcf70128f188401f0f72a4941918fc33c",
"pubkey": "828fdd0022c71558a38c0c613207ebe98d8425c3c352c3cd12e767f43506adda",
"created_at": 1774978044,
"kind": 1,
"tags": [
[
"p",
"0fb8489d1bda51d0f9c32dc008ce4878b140d614612cbb83d62c3224854e529f"
],
[
"p",
"3f7515c818bf1e76ec624c355ab22e2408d902b66824651afad01a67a856af4a"
],
[
"p",
"9a6a1a8eefd0b53d7e0c966ab35bd904151246f03b1be98fa0d2d0eeb4940320"
],
[
"p",
"608dd7b22ade794b0dde29cb84cffd69bf9f9cd477002e838206c68cb799ecb8"
],
[
"e",
"22962dfc8f9d6f083de25bb64fc91b64f035f97550d0e8f7789f801aea51a0c2",
"",
"root",
"9a6a1a8eefd0b53d7e0c966ab35bd904151246f03b1be98fa0d2d0eeb4940320"
],
[
"p",
"67f17e59b525a7cc73f7a2bb4308053daa9c4db30d42b9fcb237903d4a93043f"
],
[
"p",
"af69ea53a8f8a39e332be10e2f1954edba2aabe860d1619c125769445c2eee7e"
],
[
"proxy",
"https://mathstodon.xyz/@cbaberle/116324961130512437",
"web"
],
[
"e",
"301e356f8afcb20252bb8788559ff6a1f21e0eed4d00b3f42c5b3e0103f89881",
"",
"reply",
"9a6a1a8eefd0b53d7e0c966ab35bd904151246f03b1be98fa0d2d0eeb4940320"
],
[
"proxy",
"https://mathstodon.xyz/users/cbaberle/statuses/116324961130512437",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/cbaberle/statuses/116324961130512437",
"pink.momostr"
],
[
"-"
]
],
"content": "Having spent several years in the trenches of formalized mathematics by now, I'm actually more sympathetic nostr:npub1nf4p4rh06z6n6lsvje4txk7eqs23y3hs8vd7nraq6tgwady5qvsqy3nqe4 '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.\n\nThe 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.\n\nAs 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.\n\nThe 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.\n\nnostr:npub18a63tjqchu08dmrzfs644v3wysydjq4kdqjx2xh66qdx02zk4a9qtkszuj nostr:npub1vlchukd4yknuculh52a5xzq98k4fcndnp4ptnl9jx7gr6j5nqsls06mzqq nostr:npub14a5755aglz3euvetuy8z7x25akaz42lgvrgkr8qj2a55ghpwaelqjf9fse [@JacquesC2](https://types.pl/@JacquesC2 ) [@pigworker](https://types.pl/@pigworker ) nostr:npub1vzxa0v32meu5krw7989cfnladxlel8x5wuqzaquzqmrgedueajuq7fncd7",
"sig": "76d0cf338dc8b1eb33295cfb1e2d6d584cf3e0d4cd825a397463fa1fa79dcf34fa40ade8b60d8ff6c24b20bc38f68d8f0a604f955cfe984ac3bba9f2e7b1f9b7"
}