nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyry2ysn5av9pr8m76kgpggcflz294t0pr9shd99kh8redys7ku0xkefw8t5 (nprofile…w8t5) I wasn't thinking of bugs (your last sentence). I am coming from having never used a proof assistant. I've derived formulas for publications, but I've never published a 'proof'. Proofs are not something an astrophysicist typically does.
I think what you are saying is that if someone publishes a proof along with their proof-assistant source code, then I know that the formal computations are correct, but they may be the wrong formal computations. Perhaps the statement proven is not the statement needing to be proven.
Have I got it?
An example would be interesting.
Skewray Research
npub1jg…0ye3r
2025-12-20 01:15:47 UTC
in reply to nevent1q…3qsy
Author Public Key
npub1jgt4v6quksr3jfvvpldjqgqkg0kr7dk6wymzy4pj66794hnkjfnsc0ye3rSeen on
wss://relay.ditto.pubPublished at
2025-12-20 01:15:47 UTCEvent JSON
{
"id": "bc243a3ad706668f28ceb59c647f65886f469fcd1cb92379549b95e16812ce76",
"pubkey": "921756681cb40719258c0fdb20201643ec3f36da7136225432d6bc5ade769267",
"created_at": 1766193347,
"kind": 1,
"tags": [
[
"p",
"c8a24274eb0a119f7ed590142309f8945aade119617694b6b9c796921eb71e6b",
"wss://relay.ditto.pub/"
],
[
"p",
"5c675fe7561c52f2c0ea8db391d2c3a46556bec9a3c0a4b4f10f234fe03f58ca",
"wss://relay.ditto.pub/"
],
[
"e",
"3a511e0ca22a454db5c4b028f4a82a3a81484c42ef53bd78f3a9c62e21af6e2d",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/skewray/statuses/115749247218141464",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyry2ysn5av9pr8m76kgpggcflz294t0pr9shd99kh8redys7ku0xkefw8t5 I wasn't thinking of bugs (your last sentence). I am coming from having never used a proof assistant. I've derived formulas for publications, but I've never published a 'proof'. Proofs are not something an astrophysicist typically does.\n\nI think what you are saying is that if someone publishes a proof along with their proof-assistant source code, then I know that the formal computations are correct, but they may be the wrong formal computations. Perhaps the statement proven is not the statement needing to be proven.\n\nHave I got it?\n\nAn example would be interesting.",
"sig": "d64142f9c784e81e737059cd3bce75e2c57b806811c2c3ae04801a8444b7bdf62dc9602f7336107e47f194c7b25222bd96d9e9b9dc2840441a9b082afbf24fa2"
}