ATProto Browser

ATProto Browser

Experimental browser for the Atmosphere

Post

This is a fantastic public lecture on the role of proof assistants, gen AI and machine learning in contemporary mathematics. We were thrilled to see Lean highlighted several times - especially in its role addressing the "trust bottleneck" in maths research! #leanlang #leanprover #mathematics

Feb 25, 2025, 8:06 PM

Record data

{
  "uri": "at://did:plc:devnu4zs2viutk26clxykpbb/app.bsky.feed.post/3liznz7tqdk2y",
  "cid": "bafyreiaoeawnuzmqvu4mseo2gr7j6phh3f3mg3redejw3qci4oqi5fwhpi",
  "value": {
    "text": "This is a fantastic public lecture on the role of proof assistants, gen AI and machine learning in contemporary mathematics. We were thrilled to see Lean highlighted several times - especially in its role addressing the \"trust bottleneck\" in maths research!\n\n#leanlang #leanprover #mathematics",
    "$type": "app.bsky.feed.post",
    "embed": {
      "$type": "app.bsky.embed.record",
      "record": {
        "cid": "bafyreici7owbbspzszv6zjtancj2pvz7ribyxs64v2ejo4ziyj47utel6m",
        "uri": "at://did:plc:sr7gktoswdiw4bawp26xfrdx/app.bsky.feed.post/3lipbrgpark2r"
      }
    },
    "langs": [
      "en"
    ],
    "facets": [
      {
        "index": {
          "byteEnd": 268,
          "byteStart": 259
        },
        "features": [
          {
            "tag": "leanlang",
            "$type": "app.bsky.richtext.facet#tag"
          }
        ]
      },
      {
        "index": {
          "byteEnd": 280,
          "byteStart": 269
        },
        "features": [
          {
            "tag": "leanprover",
            "$type": "app.bsky.richtext.facet#tag"
          }
        ]
      },
      {
        "index": {
          "byteEnd": 293,
          "byteStart": 281
        },
        "features": [
          {
            "tag": "mathematics",
            "$type": "app.bsky.richtext.facet#tag"
          }
        ]
      }
    ],
    "createdAt": "2025-02-25T20:06:34.399Z"
  }
}