{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreibyo4sy2dp33k2ckjlqwophuotyctunwegavuczuntmgldgkbebp4",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mk57ztnig362"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiflo6xt7is6b2iafwghkjahlgggocme5jwjsbeuqqwcywuvjhmszm"
    },
    "mimeType": "image/png",
    "size": 24783
  },
  "path": "/abs/2604.20807v1",
  "publishedAt": "2026-04-23T00:00:00.000Z",
  "site": "https://arxiv.org",
  "tags": [
    "Mohammad Abdulaziz",
    "Thomas Ammer"
  ],
  "textContent": "**Authors:** Mohammad Abdulaziz, Thomas Ammer\n\nWe present an ongoing effort to build a framework and a library in Isabelle/HOL for formalising primal-dual arguments for the analysis of algorithms. We discuss a number of example formalisations from the theory of matching algorithms, covering classical algorithms like the Hungarian Method, widely considered the first primal-dual algorithm, and modern algorithms like the Adwords algorithm, which models the assignment of search queries to advertisers in the context of search engines.",
  "title": "Formal Primal-Dual Algorithm Analysis"
}