website-toots/109764840432564992.md

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 avatar avatar_static header header_static noindex roles 108219415927856966 brozek brozek Brandon Rozek https://fosstodon.org/@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 type author_name author_url provider_name provider_url html width height image embed_url blurhash 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. Let’s 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 doesn’t matter if it is $p$ rather than $q$ that holds, in the end $r$ holds. link Brandon Rozek https://brandonrozek.com/ 0 0 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 >}}