corpus.blog
41554 blogs · 4,644,446 posts Claim your blog
Record · corpus.blog/posts/01a08c64-c3f6-72c3-8b1b-7a87b7bf3679

Formalization of Erdős problems

Xena | Mathematicians learning Lean by doing. · published 5 December 2025

A record is what was published and who pointed at it. The text of the post is not held here: read it at the source, or at its Wayback capture.

Read the post at xenaproject.wordpress.com Wayback capture
1blogs citing
First cited
1 Feb 2026
Most recent
1 Feb 2026
Rank this month
not ranked
Links from this post
59
Words captured
3,155

Cited by

Blog
In the post
Date
David Oks | Substack
Oks notes #2: AI math, the Epstein emails, and why Steve Jobs wanted to buy General Motors Read at the source ↗
1 Feb 2026

Links from this post

Link
Host
https://borisalexeev.com/
borisalexeev.com
https://en.wikipedia.org/wiki/Paul_Erd%C5%91s
en.wikipedia.org
https://www.reddit.com/r/math/comments/13wnroa/erd%C5%91s_famously_asked_lots_of_questions_and_made/
reddit.com
https://www.erdosproblems.com/
erdosproblems.com
https://github.com/google-deepmind/formal-conjectures
github.com
https://terrytao.wordpress.com/2025/08/31/a-crowdsourced-project-to-link-up-erdosproblems-com-to-the-oeis/
terrytao.wordpress.com
http://erdosproblems.com
erdosproblems.com
https://terrytao.wordpress.com/2024/09/03/planar-point-sets-with-forbidden-four-point-patterns-and-few-distinct-distances/
terrytao.wordpress.com
https://mathoverflow.net/a/500749/1079
mathoverflow.net
https://github.com/teorth/erdosproblems/raw/main/data/statistics_history_light.svg
github.com
https://ems.press/journals/jems/articles/14297980
ems.press
https://www.erdosproblems.com/47
erdosproblems.com
https://xenaproject.wordpress.com/2023/11/04/formalising-modern-research-mathematics-in-real-time/
xenaproject.wordpress.com
https://www.erdosproblems.com/77
erdosproblems.com
https://arxiv.org/abs/2403.17370
arxiv.org
https://www.erdosproblems.com/216
erdosproblems.com
https://github.com/vasnesterov/HadwigerNelson
github.com
https://www.erdosproblems.com/508
erdosproblems.com
https://github.com/google-deepmind/formal-conjectures/blob/0f3501689b408763d86f329024f0ced8c8224356/FormalConjectures/ErdosProblems/316.lean
github.com
https://www.erdosproblems.com/316
erdosproblems.com
https://www.erdosproblems.com/379
erdosproblems.com
https://www.erdosproblems.com/987
erdosproblems.com
Formal or not formal? That is the question in AI for theorem proving. Read at the source ↗
xenaproject.wordpress.com
https://arxiv.org/abs/2510.19804
arxiv.org
https://borisalexeev.com/papers/erdos707.html
borisalexeev.com
https://www.argmin.net/p/the-fine-art-of-crate-digging
argmin.net
https://www.erdosproblems.com/707
erdosproblems.com
https://arxiv.org/pdf/2510.19804
arxiv.org
https://mathstodon.xyz/@tao/115416208975810074
mathstodon.xyz
https://mathstodon.xyz/@tao/115493667607261044
mathstodon.xyz
https://chatgpt.com/share/690a65b3-473c-800e-afa5-e99f78610ee9
chatgpt.com
https://www.erdosproblems.com/613
erdosproblems.com
https://harmonic.fun/
harmonic.fun
https://aristotle.harmonic.fun/
aristotle.harmonic.fun
https://www.erdosproblems.com/105
erdosproblems.com
https://arxiv.org/pdf/2511.14653
arxiv.org
https://mathstodon.xyz/@tao/115591487350860999
mathstodon.xyz
https://www.erdosproblems.com/367
erdosproblems.com
https://www.erdosproblems.com/418
erdosproblems.com
https://github.com/plby/lean-proofs/
github.com
https://www.erdosproblems.com/645
erdosproblems.com
https://github.com/teorth/erdosproblems/
github.com
https://arxiv.org/abs/2510.01346
arxiv.org
https://www.erdosproblems.com/488
erdosproblems.com
https://www.erdosproblems.com/124
erdosproblems.com
https://www.erdosproblems.com/481
erdosproblems.com
https://www.erdosproblems.com/730
erdosproblems.com
https://www.erdosproblems.com/198
erdosproblems.com
https://arxiv.org/abs/2511.22570v1
arxiv.org
https://www.nature.com/articles/s41586-025-09833-y
nature.com
https://arxiv.org/pdf/2511.16072
arxiv.org
https://www.erdosproblems.com/848
erdosproblems.com
https://github.com/google-deepmind/formal-conjectures/issues?q=Erd%C5%91s%20is%3Aissue%20label%3Amisformalization%20author%3Aplby
github.com
https://www.erdosproblems.com/480
erdosproblems.com
https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/
xenaproject.wordpress.com
https://althofer.de/levon-erdos-ahlswede-1996-small.jpg
althofer.de
https://www.erdosproblems.com/56
erdosproblems.com
https://mathweb.ucsd.edu/~ronspubs/96_05_integer_powers.pdf
mathweb.ucsd.edu
https://github.com/leanprover-community/mathlib4
github.com