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

12/5/2025, 4:23:32 PM

Public

Over on Kevin Buzzard's blog, Boris Alexeev has written a guest post on the state of the art on autoformalization in practice, focusing in particular on the improved speed and efficiency of formalization when applied to the problems in the Erdos Problems database, and how these efforts have begun to resolve some of the lower hanging fruit in that database. https://xenaproject.wordpress.com/2025/12/05/formalization-of-erdos-problems/

Formalization of Erdős problems

[This is a guest post by Boris Alexeev. Now over to Boris.] I’m here to tell you about various exciting developments centering on Erdős problems, especially involving the formalization of old and n…

xenaproject.wordpress.com · Xena

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