website-toots/109764840432564992.md

---
{"id": "109764840432564992", "in_reply_to_id": null, "in_reply_to_account_id": null, "sensitive": false, "spoiler_text": "", "visibility": "public", "language": "en", "replies_count": 0, "reblogs_count": 0, "favourites_count": 0, "edited_at": null, "reblog": null, "application": null, "account": {"id": "108219415927856966", "username": "brozek", "acct": "brozek", "display_name": "Brandon Rozek", "url": "https://fosstodon.org/@brozek", "uri": "https://fosstodon.org/users/brozek", "avatar": "https://cdn.fosstodon.org/accounts/avatars/108/219/415/927/856/966/original/bae9f46f23936e79.jpg", "avatar_static": "https://cdn.fosstodon.org/accounts/avatars/108/219/415/927/856/966/original/bae9f46f23936e79.jpg", "header": "https://fosstodon.org/headers/original/missing.png", "header_static": "https://fosstodon.org/headers/original/missing.png", "noindex": true, "roles": []}, "media_attachments": [], "mentions": [], "tags": [{"name": "leanprover", "url": "https://fosstodon.org/tags/leanprover"}, {"name": "itp", "url": "https://fosstodon.org/tags/itp"}, {"name": "formalmethods", "url": "https://fosstodon.org/tags/formalmethods"}], "emojis": [], "card": {"url": "https://brandonrozek.com/blog/readable-lean3-proofs/", "title": "Readable Lean 3 Proofs", "description": "Important Note: This blog post uses the Lean 3 syntax\nInteractive theorem provers are notorious for showcasing unreadable proofs. Let\u2019s illustrate our point with a couple examples and discuss various ways we can make it more readable.\nDisjunction Elimination Disjunction Elimination or proof by cases is a rule of inference that states the following. Consider you have the following three proofs:\n$p \\vee q$ $p \\rightarrow r$ $q \\rightarrow r$ Then it doesn\u2019t matter if it is $p$ rather than $q$ that holds, in the end $r$ holds.", "language": "en", "type": "link", "author_name": "Brandon Rozek", "author_url": "https://brandonrozek.com/", "provider_name": "", "provider_url": "", "html": "", "width": 0, "height": 0, "image": null, "image_description": "", "embed_url": "", "blurhash": null, "published_at": null}, "poll": null, "syndication": "https://fosstodon.org/@brozek/109764840432564992", "date": "2023-01-28T04:02:26.641Z"}
---
{{< unsafe >}}
<p>How do you organize your Lean proofs? I wrote a blog post discussing some strategies I employ to make Lean 3 proofs more readable.</p><p><a href="https://brandonrozek.com/blog/readable-lean3-proofs/" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">brandonrozek.com/blog/readable</span><span class="invisible">-lean3-proofs/</span></a></p><p><a href="https://fosstodon.org/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://fosstodon.org/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://fosstodon.org/tags/FormalMethods" class="mention hashtag" rel="tag">#<span>FormalMethods</span></a></p>
{{< /unsafe >}}