tqft retweeted
The Lean FRO Year 4 Part 1 roadmap, covering September 2026 through February 2027, is now published. It sets out our priorities for Lean and ecosystem support for the first half of our fourth year of operations.
🔗 Read the full roadmap here: lean-lang.org/fro/roadmap/y4…
#LeanLang #LeanProver
Today we're launching the Palomar registry at palomar-registry.org/, an index of formalized mathematics results.
If you have a GitHub repo with some maths, and can set up github.com/leanprover/compar… for verification and github.com/mathlib-initiativ… for metadata, please submit!
Take a look at Terry Tao's announcement post at terrytao.wordpress.com/2026/…
@CadeMetz, I was disappointed by your article nytimes.com/2023/02/16/techn…, which seems to beg the question.
I would like to see you explain why Sydney is not sentient in a manner which nevertheless allows humans to be counted as sentient!
1/3
The substantive descriptions you provide of modern LLMs seem to apply equally well to human intelligence:
"neural networks that learned from enormous amounts of digital text, including books"
"a [...] system that learns skills by analyzing vast amounts of [...] data"
2/3
tqft retweeted
sbseminar.wordpress.com/2017… #Elsevier change their licence AFTER publication. Get bloody angry. Walk away from Elsevier.
@mikedimpact, yup it's me. (Not actually that active on twitter, mostly just playing with new iOS 5 apps.)
Given only an afternoon in Tuolumne, Matthes Crest 4:15 car-to-car was fun. The driving less so; disappointed.