tqft

Mathematics for Programming, Programming for Mathematics

I work on the Lean Theorem Prover, for the Lean FRO.

[tqft @tqft]

@ElliotGlazer @IlinVasily29521 @JasonRute @ElliotGlazer not yet for Risch. I read up on it, but haven't added anything to https://t.co/WnuSxoj6N6 yet. A paragraph there, or a detailed SPEC, would be a welcome PR!

[tqft @tqft]

@leanprover * Palomar https://t.co/dBr0M9TQMv, our new registry for Lean-verified formal proof projects

* Hex https://t.co/We0S9IQkOk, computer algebra in Lean, which has recently released fast integer polynomial factorization and lattice basis reduction algorithms, with many more to come

[tqft @tqft]

@leanprover along with some of my projects:

* Tau Ceti https://t.co/utdVi21CPY, the AI-driven library of formal mathematics downstream of mathlib (see my blog post about 10 theorems that recently landed in Tau Ceti at https://t.co/vUHl5XLZDN)

[tqft @tqft]

@leanprover There's so much cool stuff in here:

* the Lean Workbench https://t.co/Xx30KtssVR (zero install Lean workspaces)

* `bv_decide`, our bitvector decision procedure, is fast: https://t.co/pMCfbj4UPe

* Nerodia https://t.co/EA3B4EmwEm, deploy Lean libraries as Python!

[Lean @leanprover]

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: https://t.co/jNwxFSqsdW

#LeanLang #LeanProver

[tqft @tqft]

@ElliotGlazer Palomar doesn't host your code, but it *does* make a fork of your repository (and its dependencies) at https://t.co/Ty5BLfP74o, so submissions do survive repositories being deleting, rewritten, or made private. (But don't survive Github going down, or a takedown.)

[tqft @tqft]

Or join us on the Lean zulip to discuss: https://t.co/XofBigvDbq

[tqft @tqft]

Today we're launching the Palomar registry at https://t.co/dBr0M9TQMv, an index of formalized mathematics results.

If you have a GitHub repo with some maths, and can set up https://t.co/UCLgkPC9lu for verification and https://t.co/FDSmIK5LJa for metadata, please submit!

[tqft @tqft]

Take a look at Terry Tao's announcement post at https://t.co/3fzXBh7Wq5

[tqft @tqft]

@__alpoge__ And now fully formalized in Lean at https://t.co/mmm9pWkrdd

[tqft @tqft]

I fear that too many people are secretly thinking "LLMs are not sentient because they don't have souls".

It's hard to tell from your output token stream whether you would recognise that as bullsh*t or not.

3/3

[tqft @tqft]

@CadeMetz, I was disappointed by your article https://t.co/0j3oJ0U4Kf, 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

[tqft @tqft]

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 @tqft]

@LGBTMath I noticed on the “History” page (https://t.co/8AcoD7xTQG) the link to the article in the notices is broken. I think the correct URL is https://t.co/AT5UJQuexM

[Peter Murray-Rust @petermurrayrust]

https://t.co/aDvTjBjhtP #Elsevier change their licence AFTER publication. Get bloody angry. Walk away from Elsevier.

[tqft @tqft]

@ElsevierConnect, what happened to our right to redistribute the mathematics open archive? https://t.co/FcIRSxMKOR

[tqft @tqft]

@theWinnower 2/2 Does it make legal sense for one to by exclusively licensed to a publisher, with the other creative commons?

[tqft @tqft]

@theWinnower Could you blog about the legal distinction between copyright in author-accepted vs published versions? ... 1/2

[tqft @tqft]

@astrobonnie wait until you get to add X% committee meetings!

[tqft @tqft]

@digitalocean An account at your Amsterdam data centre has been attacking our servers (https://t.co/oHYKmXcXRQ ). Can we coordinate?