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`

Terence Tao @tao@mathstodon.xyz

5/31/2025, 5:23:59 PM

Public

I have just launched a "Lean companion" to my real analysis undergraduate textbook "Analysis I" at https://github.com/teorth/analysis . This gives a Lean translation (or paraphrasing) of the various definitions, theorems, and exercises in the textbook into Lean, thus allowing for an alternate way for students to work through the text. It is also designed to gradually transition into the standard Lean library Mathlib, thus also potentially serving as an introduction to that library as well.

Further discussion at https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/

GitHub - teorth/analysis

Contribute to teorth/analysis development by creating an account on GitHub.

github.com · GitHub

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