not quite. most mathematicians pretend they work with ZFC but can't state the axioms. they (we) just work with a naive notion of set and the habit not to write something blatantly inconsistent.
of course, every large formalization effort brings some technical debt.
in the 80s, Pierre Cartier explained in several interviews why Bourbaki didn't make the move to categories some 20 years before while they (Cartan, Eilenberg) had basically if not invented them, then making them prominent: that would have meant rewriting 2000 pages and they felt they had better write down their ideas about Lie groups and Lie algebras.
⏚ Antoine Chambert-Loir
npub1j7…6a4dl
2024-12-17 22:00:47 UTC
in reply to nevent1q…af4e
Author Public Key
npub1j7kvjvr8hkvwzvs889v2ycwpvh0n7qns5ha84xzh2r36zrakk4wsc6a4dlSeen on
wss://relay.momostr.pinkPublished at
2024-12-17 22:00:47 UTCEvent JSON
{
"id": "3d5673e93a46244897a284cf563089efdef982a49ec4e6a7c6f446fb6b4931b3",
"pubkey": "97acc93067bd98e132073958a261c165df3f0270a5fa7a985750e3a10fb6b55d",
"created_at": 1734472847,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/@antoinechambertloir/113670412516516580",
"web"
],
[
"p",
"9a6a1a8eefd0b53d7e0c966ab35bd904151246f03b1be98fa0d2d0eeb4940320"
],
[
"e",
"8acd325b42988686cac686cd892b548219845135779752b98b08f609bb05c372",
"",
"reply",
"9a6a1a8eefd0b53d7e0c966ab35bd904151246f03b1be98fa0d2d0eeb4940320"
],
[
"e",
"59e56f0b056ac2e33ca2bb8e13bbeee9afc9da177e0b08715fdf05023cf59f5a",
"",
"root",
"75c7d1f69389e4c76276bb851aea7f54265d145c7a39678589cfd62ce26ae9b3"
],
[
"p",
"75c7d1f69389e4c76276bb851aea7f54265d145c7a39678589cfd62ce26ae9b3"
],
[
"proxy",
"https://mathstodon.xyz/users/antoinechambertloir/statuses/113670412516516580",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/antoinechambertloir/statuses/113670412516516580",
"pink.momostr"
],
[
"-"
]
],
"content": "not quite. most mathematicians pretend they work with ZFC but can't state the axioms. they (we) just work with a naive notion of set and the habit not to write something blatantly inconsistent.\nof course, every large formalization effort brings some technical debt. \nin the 80s, Pierre Cartier explained in several interviews why Bourbaki didn't make the move to categories some 20 years before while they (Cartan, Eilenberg) had basically if not invented them, then making them prominent: that would have meant rewriting 2000 pages and they felt they had better write down their ideas about Lie groups and Lie algebras.",
"sig": "1a48d6975122c68d4b19b4d16c5256261abdeafdff0422419532ef8f1770c6015cc8db72db81170fc813c8d6507e3a711f2ad33cac48502f8d019e471cda19a4"
}