#mathlib — Public Fediverse posts

So, just double-checking how #Lean4 and #Mathlib work:

* Lean takes 3GiB of RAM and a minute to open Mathlib
* Lean requires about 10min to build itself in CI, only verifying required theorems
* Verifying all of Mathlib is measured in hours
* Lean's kernel is untrustworthy due to junk theorems

And yet I'm a clown for using #Metamath? At some point we ought to reconsider the type-theory fetish.

Lean Theorem Prover Mathlib

https://github.com/leanprover-community/mathlib4

#HackerNews #Lean #Theorem #Prover #Mathlib #mathlib4 #LeanProver #theoremProving #functionalProgramming

Readings shared October 3, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/04-readings_shared_10-03-25 #AI #ATP #AlphaProof #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Mathlib

Yapay zeka, büyük veri setlerini analiz etmekten karmaşık simülasyonlar oluşturmaya kadar, hesaplamalı matematiğin ağır işlerini üstlenerek büyük bir güç haline geldi. Şu an itibarıyla, YZ genellikle kendisine verilen ispatları adım adım doğrulayabiliyor; ancak nihai kararı ve en yaratıcı kanıt yöntemlerinin keşfini hâlâ insan zekasına bırakıyor.
Peki ya bu denge değişirse?
#YapayZeka #Matematik #AlphaProof #Lean #mathlib #DeepMind #YaşamOyunu
https://youtu.be/ZERkY5kExjI
https://monologblg.com/matematik-sadece-insana-mi-ait/