website-toots/109764840432564992.md
GitHub Actions Bot e3c67fe223 New/Modified Toots
2023-09-21 23:19:52 +00:00

2.9 KiB
Raw Blame History

id in_reply_to_id in_reply_to_account_id sensitive spoiler_text visibility language replies_count reblogs_count favourites_count edited_at reblog application account media_attachments mentions tags emojis card poll syndication date
109764840432564992 null null false public en 0 0 0 null null null
id username acct display_name url uri avatar avatar_static header header_static noindex roles
108219415927856966 brozek brozek Brandon Rozek https://fosstodon.org/@brozek https://fosstodon.org/users/brozek https://cdn.fosstodon.org/accounts/avatars/108/219/415/927/856/966/original/bae9f46f23936e79.jpg https://cdn.fosstodon.org/accounts/avatars/108/219/415/927/856/966/original/bae9f46f23936e79.jpg https://fosstodon.org/headers/original/missing.png https://fosstodon.org/headers/original/missing.png true
name url
leanprover https://fosstodon.org/tags/leanprover
name url
itp https://fosstodon.org/tags/itp
name url
formalmethods https://fosstodon.org/tags/formalmethods
url title description language type author_name author_url provider_name provider_url html width height image image_description embed_url blurhash published_at
https://brandonrozek.com/blog/readable-lean3-proofs/ Readable Lean 3 Proofs Important Note: This blog post uses the Lean 3 syntax Interactive theorem provers are notorious for showcasing unreadable proofs. Lets illustrate our point with a couple examples and discuss various ways we can make it more readable. Disjunction Elimination Disjunction Elimination or proof by cases is a rule of inference that states the following. Consider you have the following three proofs: $p \vee q$ $p \rightarrow r$ $q \rightarrow r$ Then it doesnt matter if it is $p$ rather than $q$ that holds, in the end $r$ holds. en link Brandon Rozek https://brandonrozek.com/ 0 0 null null null
null https://fosstodon.org/@brozek/109764840432564992 2023-01-28T04:02:26.641Z

{{< unsafe >}}

How do you organize your Lean proofs? I wrote a blog post discussing some strategies I employ to make Lean 3 proofs more readable.

https://brandonrozek.com/blog/readable-lean3-proofs/

#LeanProver #ITP #FormalMethods

{{< /unsafe >}}