A small tool to view real-world ActivityPub objects as JSON! Enter a URL
or username from Mastodon or a similar service below, and we'll send a
request with
the right
Accept
header
to the server to view the underlying object.
{
"@context": [
"https://www.w3.org/ns/activitystreams",
{
"ostatus": "http://ostatus.org#",
"atomUri": "ostatus:atomUri",
"inReplyToAtomUri": "ostatus:inReplyToAtomUri",
"conversation": "ostatus:conversation",
"sensitive": "as:sensitive",
"toot": "http://joinmastodon.org/ns#",
"votersCount": "toot:votersCount",
"Hashtag": "as:Hashtag"
}
],
"id": "https://mathstodon.xyz/users/tao/statuses/114486537464033675",
"type": "Note",
"summary": null,
"inReplyTo": null,
"published": "2025-05-11T01:12:05Z",
"url": "https://mathstodon.xyz/@tao/114486537464033675",
"attributedTo": "https://mathstodon.xyz/users/tao",
"to": [
"https://www.w3.org/ns/activitystreams#Public"
],
"cc": [
"https://mathstodon.xyz/users/tao/followers"
],
"sensitive": false,
"atomUri": "https://mathstodon.xyz/users/tao/statuses/114486537464033675",
"inReplyToAtomUri": null,
"conversation": "tag:mathstodon.xyz,2025-05-11:objectId=152622576:objectType=Conversation",
"content": "<p>I recently set myself the exercise of using modern automated tools - in particular, a combination of the <a href=\"https://mathstodon.xyz/tags/GithubCopilot\" class=\"mention hashtag\" rel=\"tag\">#<span>GithubCopilot</span></a> large language model and the dependent type matching tactic <a href=\"https://mathstodon.xyz/tags/canonical\" class=\"mention hashtag\" rel=\"tag\">#<span>canonical</span></a> - to try to semi-automatically formalize in <a href=\"https://mathstodon.xyz/tags/Lean\" class=\"mention hashtag\" rel=\"tag\">#<span>Lean</span></a> a one-page proof provided by a collaborator of the <a href=\"https://mathstodon.xyz/tags/EquationalTheoriesProject\" class=\"mention hashtag\" rel=\"tag\">#<span>EquationalTheoriesProject</span></a> (Bruno Le Floch). With these tools, I was able to more or less blindly do the formalization in 33 minutes, withou any real high level conception of how the proof proceeded. It was a very different style to how I usually formalize results, but was workable for this type of technical, non-conceptual argument where the main issue is to get the details correct rather than the "big picture".</p><p>I recorded my attempt at <a href=\"https://www.youtube.com/watch?v=cyyR7j2ChCI\" target=\"_blank\" rel=\"nofollow noopener noreferrer\" translate=\"no\"><span class=\"invisible\">https://www.</span><span class=\"ellipsis\">youtube.com/watch?v=cyyR7j2ChC</span><span class=\"invisible\">I</span></a> . See also additional discussion at <a href=\"https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Alternative.20proofs.20of.20E1689.E2.8A.A2E2\" target=\"_blank\" rel=\"nofollow noopener noreferrer\" translate=\"no\"><span class=\"invisible\">https://</span><span class=\"ellipsis\">leanprover.zulipchat.com/#narr</span><span class=\"invisible\">ow/channel/458659-Equational/topic/Alternative.20proofs.20of.20E1689.E2.8A.A2E2</span></a> . The final proof (which is far from optimized, but got the job done) can be found at <a href=\"https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean\" target=\"_blank\" rel=\"nofollow noopener noreferrer\" translate=\"no\"><span class=\"invisible\">https://</span><span class=\"ellipsis\">github.com/teorth/estimate_too</span><span class=\"invisible\">ls/blob/master/EstimateTools/test/equational.lean</span></a></p>",
"contentMap": {
"en": "<p>I recently set myself the exercise of using modern automated tools - in particular, a combination of the <a href=\"https://mathstodon.xyz/tags/GithubCopilot\" class=\"mention hashtag\" rel=\"tag\">#<span>GithubCopilot</span></a> large language model and the dependent type matching tactic <a href=\"https://mathstodon.xyz/tags/canonical\" class=\"mention hashtag\" rel=\"tag\">#<span>canonical</span></a> - to try to semi-automatically formalize in <a href=\"https://mathstodon.xyz/tags/Lean\" class=\"mention hashtag\" rel=\"tag\">#<span>Lean</span></a> a one-page proof provided by a collaborator of the <a href=\"https://mathstodon.xyz/tags/EquationalTheoriesProject\" class=\"mention hashtag\" rel=\"tag\">#<span>EquationalTheoriesProject</span></a> (Bruno Le Floch). With these tools, I was able to more or less blindly do the formalization in 33 minutes, withou any real high level conception of how the proof proceeded. It was a very different style to how I usually formalize results, but was workable for this type of technical, non-conceptual argument where the main issue is to get the details correct rather than the "big picture".</p><p>I recorded my attempt at <a href=\"https://www.youtube.com/watch?v=cyyR7j2ChCI\" target=\"_blank\" rel=\"nofollow noopener noreferrer\" translate=\"no\"><span class=\"invisible\">https://www.</span><span class=\"ellipsis\">youtube.com/watch?v=cyyR7j2ChC</span><span class=\"invisible\">I</span></a> . See also additional discussion at <a href=\"https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Alternative.20proofs.20of.20E1689.E2.8A.A2E2\" target=\"_blank\" rel=\"nofollow noopener noreferrer\" translate=\"no\"><span class=\"invisible\">https://</span><span class=\"ellipsis\">leanprover.zulipchat.com/#narr</span><span class=\"invisible\">ow/channel/458659-Equational/topic/Alternative.20proofs.20of.20E1689.E2.8A.A2E2</span></a> . The final proof (which is far from optimized, but got the job done) can be found at <a href=\"https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean\" target=\"_blank\" rel=\"nofollow noopener noreferrer\" translate=\"no\"><span class=\"invisible\">https://</span><span class=\"ellipsis\">github.com/teorth/estimate_too</span><span class=\"invisible\">ls/blob/master/EstimateTools/test/equational.lean</span></a></p>"
},
"attachment": [],
"tag": [
{
"type": "Hashtag",
"href": "https://mathstodon.xyz/tags/equationaltheoriesproject",
"name": "#equationaltheoriesproject"
},
{
"type": "Hashtag",
"href": "https://mathstodon.xyz/tags/lean",
"name": "#lean"
},
{
"type": "Hashtag",
"href": "https://mathstodon.xyz/tags/canonical",
"name": "#canonical"
},
{
"type": "Hashtag",
"href": "https://mathstodon.xyz/tags/githubcopilot",
"name": "#githubcopilot"
}
],
"replies": {
"id": "https://mathstodon.xyz/users/tao/statuses/114486537464033675/replies",
"type": "Collection",
"first": {
"type": "CollectionPage",
"next": "https://mathstodon.xyz/users/tao/statuses/114486537464033675/replies?only_other_accounts=true&page=true",
"partOf": "https://mathstodon.xyz/users/tao/statuses/114486537464033675/replies",
"items": []
}
},
"likes": {
"id": "https://mathstodon.xyz/users/tao/statuses/114486537464033675/likes",
"type": "Collection",
"totalItems": 57
},
"shares": {
"id": "https://mathstodon.xyz/users/tao/statuses/114486537464033675/shares",
"type": "Collection",
"totalItems": 28
}
}