Mathstodon

José A. AlonsoReadings shared April 3, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/03-readings_shared_04-03-25" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2025/04/03-readings_shared_04-03-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="tag">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a>

José A. AlonsoAlphaProof: when reinforcement learning meets formal mathematics. ~ Thomas Hubert. <a href="https://youtu.be/TFBzP78Jp6A" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://youtu.be/TFBzP78Jp6A</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a>

LavX NewsAI and the Future of Mathematical Proofs: A New Era of Collaboration and InnovationAs AI continues to evolve, the intersection of mathematics and machine learning is poised to revolutionize how proofs are generated and verified. With the advent of interactive theorem provers and adv...<a href="https://news.lavx.hu/article/ai-and-the-future-of-mathematical-proofs-a-new-era-of-collaboration-and-innovation" rel="nofollow noopener noreferrer" target="_blank">https://news.lavx.hu/article/ai-and-the-future-of-mathematical-proofs-a-new-era-of-collaboration-and-innovation</a><a href="https://mastodon.cloud/tags/news" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#news</a> <a href="https://mastodon.cloud/tags/tech" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#tech</a> <a href="https://mastodon.cloud/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://mastodon.cloud/tags/InteractiveTheoremProvers" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#InteractiveTheoremProvers</a> <a href="https://mastodon.cloud/tags/AlphaProof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AlphaProof</a>

José A. AlonsoReadings shared November 29, 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/11/29-readings_shared_11-29-24" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2024/11/29-readings_shared_11-29-24</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="tag">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="tag">#Calculemus</a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="tag">#MachineLearning</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#LLMs</a> <a href="https://mathstodon.xyz/tags/AIMO" class="mention hashtag" rel="tag">#AIMO</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/AlphaGeometry" class="mention hashtag" rel="tag">#AlphaGeometry</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#Haskell</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="tag">#Programming</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="tag">#FormalVerification</a> <a href="https://mathstodon.xyz/tags/Dafny" class="mention hashtag" rel="tag">#Dafny</a>

José A. AlonsoMachine learning and mathematics (The twin catalysts poised to accelerate twenty-first century mathematics: formalisation and machine learning). ~ Harald Carlens. <a href="https://joltml.com/ml-mathematics/" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://joltml.com/ml-mathematics/</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="tag">#MachineLearning</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#LLMs</a> <a href="https://mathstodon.xyz/tags/AIMO" class="mention hashtag" rel="tag">#AIMO</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/AlphaGeometry" class="mention hashtag" rel="tag">#AlphaGeometry</a>

Alex vd Brandhof<a href="https://mathstodon.xyz/tags/ChatGPT" class="mention hashtag" rel="tag">#ChatGPT</a> geeft soms een perfecte oplossing als je hem een wiskundevraagstuk voorlegt, inclusief heldere uitleg bij tussenstappen. Maar vaak ook bluft hij maar wat. Het probleem met ChatGPT: hij weet zélf niet wanneer hij bluft. Drie nieuwe AI-wiskundetools doen het beter: <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a>, <a href="https://mathstodon.xyz/tags/AlphaGeometry" class="mention hashtag" rel="tag">#AlphaGeometry</a> en <a href="https://mathstodon.xyz/tags/o1" class="mention hashtag" rel="tag">#o1</a>. Mijn verhaal erover voor NRC <a href="https://www.nrc.nl/nieuws/2024/10/04/ai-ontwikkelt-een-wiskundeknobbel-a4867967" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.nrc.nl/nieuws/2024/10/04/ai-ontwikkelt-een-wiskundeknobbel-a4867967</a>

José A. AlonsoReadings shared September 11, 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/09/11-readings_shared_09-11-24" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2024/09/11-readings_shared_09-11-24</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#Coq</a> <a href="https://mathstodon.xyz/tags/NaprocheZF" class="mention hashtag" rel="tag">#NaprocheZF</a> <a href="https://mathstodon.xyz/tags/Natty" class="mention hashtag" rel="tag">#Natty</a> <a href="https://mathstodon.xyz/tags/AlphaGeometry" class="mention hashtag" rel="tag">#AlphaGeometry</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/OCaml" class="mention hashtag" rel="tag">#OCaml</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="tag">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/IMO" class="mention hashtag" rel="tag">#IMO</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="tag">#MachineLearning</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#LLMs</a>

José A. AlonsoMathematical Olympiad (To the geometry and beyond...). ~ Mirek Olšák. <a href="https://aitp-conference.org/2024/slides/MO.pdf" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://aitp-conference.org/2024/slides/MO.pdf</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/IMO" class="mention hashtag" rel="tag">#IMO</a> <a href="https://mathstodon.xyz/tags/AlphaGeometry" class="mention hashtag" rel="tag">#AlphaGeometry</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#LeanProver</a>

José A. AlonsoReadings shared August 20, 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/08/21-readings_shared_08-20-24" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2024/08/21-readings_shared_08-20-24</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#Coq</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="tag">#ACL2</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#Haskell</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="tag">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="tag">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="tag">#TypeTheory</a>

José A. AlonsoImproving on AlphaProof: IMO 2024 problem 2 in Lean 4. ~ David Renshaw. <a href="https://youtu.be/5IARsdn78xE" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://youtu.be/5IARsdn78xE</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a>

Rod2ik 🇪🇺 🇨🇵 🇪🇸 🇺🇦 🇨🇦 🇩🇰 🇬🇱Deux <a href="https://mastodon.social/tags/IA" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IA</a> de <a href="https://mastodon.social/tags/Google" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Google</a> , baptisées <a href="https://mastodon.social/tags/Alphaproof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Alphaproof</a> et <a href="https://mastodon.social/tags/AlphaGeometry" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AlphaGeometry</a> 2 :ces systèmes d' <a href="https://mastodon.social/tags/IA" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IA</a> spécialisés ont résolu quatre des six problèmes présentés cette année dans le cadre de l' Olympiade Internationale de Mathématiques <a href="https://mastodon.social/tags/Google" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Google</a> revendique une percée dans ce domaine<a href="https://www.generation-nt.com/actualites/ia-google-deepmind-mathematiques-raisonnement-2049320" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.generation-nt.com/actualites/ia-google-deepmind-mathematiques-raisonnement-2049320</a>

GenAINews.coExciting news from Unite.AI about AI at the International Mathematical Olympiad! AlphaProof and AlphaGeometry 2 achieved a silver-medal standard. 🥈 <a href="https://mastodon.social/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AI</a> <a href="https://mastodon.social/tags/Mathematics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Mathematics</a> <a href="https://mastodon.social/tags/IMO" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IMO</a> <a href="https://mastodon.social/tags/AlphaProof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AlphaProof</a> <a href="https://mastodon.social/tags/AlphaGeometry2" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AlphaGeometry2</a><a href="https://www.unite.ai/ai-at-the-international-mathematical-olympiad-how-alphaproof-and-alphageometry-2-achieved-silver-medal-standard/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.unite.ai/ai-at-the-international-mathematical-olympiad-how-alphaproof-and-alphageometry-2-achieved-silver-medal-standard/</a>

Pustam | पुस्तम | পুস্তম🇳🇵AI reached the level of 12-year-old Terence Tao! Both won a Silver medal with 28 points. <a href="https://mathstodon.xyz/tags/IMO" class="mention hashtag" rel="tag">#IMO</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/Terence" class="mention hashtag" rel="tag">#Terence</a> <a href="https://mathstodon.xyz/tags/Tao" class="mention hashtag" rel="tag">#Tao</a> <a href="https://mathstodon.xyz/tags/TerenceTao" class="mention hashtag" rel="tag">#TerenceTao</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/Maths" class="mention hashtag" rel="tag">#Maths</a> <a href="https://mathstodon.xyz/tags/Olympiad" class="mention hashtag" rel="tag">#Olympiad</a> <a href="https://mathstodon.xyz/tags/Mathematics" class="mention hashtag" rel="tag">#Mathematics</a> <a href="https://mathstodon.xyz/tags/SilverMedal" class="mention hashtag" rel="tag">#SilverMedal</a> <a href="https://mathstodon.xyz/tags/DeepMind" class="mention hashtag" rel="tag">#DeepMind</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/AlphaGeometry" class="mention hashtag" rel="tag">#AlphaGeometry</a>

José A. AlonsoLecturas compartidas el 26 de julio de 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/07/27-lecturas_compartidas_el_26-jul-24" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2024/07/27-lecturas_compartidas_el_26-jul-24</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#Coq</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/IMO" class="mention hashtag" rel="tag">#IMO</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#Haskell</a>

Alessio Pomaro🧠 <a href="https://mastodon.uno/tags/DeepMind" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#DeepMind</a> ha sviluppato due nuovi modelli di intelligenza artificiale, <a href="https://mastodon.uno/tags/AlphaProof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AlphaProof</a> e <a href="https://mastodon.uno/tags/AlphaGeometry" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AlphaGeometry</a> 2, che sono riusciti a risolvere quattro dei sei problemi della International Mathematical Olympiad (IMO), raggiungendo il livello di una medaglia d'argento.  💡 Questi modelli hanno dimostrato un avanzato ragionamento matematico, con AlphaProof specializzato in algebra e teoria dei numeri, mentre AlphaGeometry 2 ha eccelso in problemi geometrici. <a href="https://mastodon.uno/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AI</a> <a href="https://mastodon.uno/tags/GenAI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#GenAI</a> <a href="https://mastodon.uno/tags/GenerativeAI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#GenerativeAI</a>

José A. AlonsoGoogle DeepMind IMO 2024 Solutions. <a href="https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/IMO" class="mention hashtag" rel="tag">#IMO</a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/AlphaGeometry2" class="mention hashtag" rel="tag">#AlphaGeometry2</a>

José A. AlonsoMove over, mathematicians, here comes AlphaProof (A.I. is getting good at math — and might soon make a worthy collaborator for humans). ~ Siobhan Roberts. <a href="https://www.nytimes.com/2024/07/25/science/ai-math-alphaproof-deepmind.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.nytimes.com/2024/07/25/science/ai-math-alphaproof-deepmind.html</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/IMO" class="mention hashtag" rel="tag">#IMO</a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="tag">#AlphaProof</a>

IT NewsGoogle claims math breakthrough with proof-solving AI models - Enlarge / An illustration provided by Google. (credit: Google) ... - <a href="https://arstechnica.com/?p=2039221" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://arstechnica.com/?p=2039221</a> <a href="https://schleuss.online/tags/machinelearning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#machinelearning</a> <a href="https://schleuss.online/tags/alphageometry2" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#alphageometry2</a> <a href="https://schleuss.online/tags/googledeepmind" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#googledeepmind</a> <a href="https://schleuss.online/tags/alphageometry" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#alphageometry</a> <a href="https://schleuss.online/tags/alphaproof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#alphaproof</a> <a href="https://schleuss.online/tags/biz" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#biz</a>⁢ <a href="https://schleuss.online/tags/google" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#google</a> <a href="https://schleuss.online/tags/ai" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ai</a>

Recent searches

Search options

Administered by:

Server stats:

#alphaproof