Hackers' Pub

Syntax	Description	Examples
`"` keyword `"`	Finds the string within quotes, including spaces. Case-insensitive. (Escape quotes inside with `\"`)	`"Hackers' Pub"`
`from:` handle	Finds content written by the specified user.	`from:hongminhee` `from:hongminhee@hollo.social`
`lang:` ISO 639-1	Finds content written in the specified language.	`lang:en`
`#` tag	Finds content with the specified tag. Case-insensitive.	`#HackersPub`
condition condition	Finds content that satisfies both conditions on either side of the space (logical AND).	`"Hackers' Pub" lang:en`
condition `OR` condition	Finds content that satisfies at least one of the conditions on either side of the OR operator (logical OR).	`#HackersPub OR "Hackers' Pub" lang:en`
`(` condition `)`	Combines the operators within the parentheses first.	`(#HackersPub OR "Hackers' Pub" OR "Hackers Pub") lang:en`

Michael Kohl 🇦🇹🇹🇭 @citizen428@chaos.social

12/26/2025, 4:07:05 PM

Public

I like this quote in "From Zero to QED":

"The honest truth is that most people do not need dependent type theory or formal verification for their day jobs. But necessity is a boring criterion for what to learn. People study ancient languages, play chess, learn to cook elaborate dishes, prove that there are infinitely many primes. The question is not whether you need something but whether it interests you."

https://sdiehl.github.io/zero-to-qed/02_why.html

#lean4

From Zero to QED: An informal introduction to formality in Lean 4

An informal introduction to formality in Lean 4

sdiehl.github.io · From Zero to QED

If you have a fediverse account, you can quote this note from your own instance. Search https://chaos.social/users/citizen428/statuses/115786725794900673 on your instance and quote it. (Note that quoting is not supported in Mastodon.)