nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqch8hfpny6tp95jqut4smklg3nx2h93dvvw6x4jsaqzwj8u6az9lq40qmju (nprofile…qmju) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqhlkl8ccw38f2nas0vvz870ay2725x4gfasysv4lkw96daq0707vsa2rrr0 (nprofile…rrr0)
I think newcomers tend to forget that proof assistants can only validate proofs.
They cannot validate mathematical definitions (other than for syntactical/type correctness).
So saying that a mathematical definition has been formalized doesn't mean much in terms of assurance.
Only a mathematician, and definitely not the proof assistant, can tell whether the mathematical definition has been correctly transcribed to the language of the proof assistant.
For instance, Gonthier explicitly made sure that the definitions were as small as possible, and as clear as possible, in his project (with many other people) to prove the 4-colour theorem formally.
Only after we know (without the assistance of the proof assistant) that our formalized definitions are correct, can we trust proofs about them.
Martin Escardo /
npub1t3…fg3z4
2025-05-29 19:35:27
in reply to nevent1q…2523
Author Public Key
npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4Seen on
wss://relay.mostr.pubPublished at
2025-05-29 19:35:27Event JSON
{
"id": "c9ebdd500ee3496172231469ab1f0fa2a131638f95897e61ff8ebe539e085962",
"pubkey": "5c675fe7561c52f2c0ea8db391d2c3a46556bec9a3c0a4b4f10f234fe03f58ca",
"created_at": 1748547327,
"kind": 1,
"tags": [
[
"p",
"c5cf748664d2c25a481c5d61bb7d11999572c5ac63b46aca1d009d23f35d117e",
"wss://relay.mostr.pub"
],
[
"p",
"bfedf3e30e89d2a9f60f63047f3fa45795435509ec090657f67174de81fe7f99",
"wss://relay.mostr.pub"
],
[
"p",
"8c5f80dac33dcd913311c7513d86a1b1009732ce9b879fa0b08480a260fbeb47",
"wss://relay.mostr.pub"
],
[
"p",
"bc13e579bf49294633747700e25eb4f71d0c2aa134e89f30d36d7e1630e1bba3",
"wss://relay.mostr.pub"
],
[
"e",
"7c17fc6d75f6ff95af049de8d4a92af71de392434cb12889f5cc7d2505227033",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/MartinEscardo/statuses/114592797668397422",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqch8hfpny6tp95jqut4smklg3nx2h93dvvw6x4jsaqzwj8u6az9lq40qmju nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqhlkl8ccw38f2nas0vvz870ay2725x4gfasysv4lkw96daq0707vsa2rrr0 \n\nI think newcomers tend to forget that proof assistants can only validate proofs.\n\nThey cannot validate mathematical definitions (other than for syntactical/type correctness).\n\nSo saying that a mathematical definition has been formalized doesn't mean much in terms of assurance.\n\nOnly a mathematician, and definitely not the proof assistant, can tell whether the mathematical definition has been correctly transcribed to the language of the proof assistant.\n\nFor instance, Gonthier explicitly made sure that the definitions were as small as possible, and as clear as possible, in his project (with many other people) to prove the 4-colour theorem formally.\n\nOnly after we know (without the assistance of the proof assistant) that our formalized definitions are correct, can we trust proofs about them.",
"sig": "c618c81b5c20c30dc6385fd9e7a38e4aac12d3ae588db8d290027d3f69cd331e9eaee421be7ac7cca52f94f5de3dbd88c37366169fe48e0921120d9bce9c22dc"
}