This happened to me with idris and many others, I took some time to learn the basics, wrote some examples and then FFI was a joke or code generators for JavaScript absolutely useless.
So no way of leveraging an existing ecosystem.
“The current interface was designed for internal use in Lean and should be considered unstable. It will be refined and extended in the future.“
My point is that in order to use these problem provers you really gotta be sure you need them, otherwise interaction with an external ecosystem might be a dep/compilation nightmare or bridge over tcp just to use libraries.
When you ground a system in formalized logic rather than probabilistic weights, you don't just get better results; you get mathematical guarantees. Relying on continuous approximation is fine for chat, but building truly robust systems requires discrete, deterministic proofs. This is exactly the paradigm shift needed.
[1] https://old.reddit.com/r/totallynotrobots
PS: Of course that's not true. An ID system for humans will inevitably become mandatory and, naturally, politicians will soon enough create a reason to use it for enforcing a planet wide totalitarian government watched over by Big Brother.
Conspiracy-theory-nonsense? Maybe! I'll invite some billionaires to pizza and ask them what they think.
- Lean supports calling out as a tactic, allowing you to call LLMs or other AI as judges (ie, they return a judgment about a claim)
- Lean can combine these judgments from external systems according to formal theories (ie, normal proof mechanics)
- an LLM engaged in higher order reasoning can decompose its thinking into such logical steps of fuzzy blocks
- this can be done recursively, eg, having a step that replaces LLM judgments with further logical formulations of fuzzy judgments from the LLM
Something, something, sheaves.
throwaway2027•1h ago
seanhunter•1h ago
https://github.com/teorth/analysis
He also has blogged about how he uses lean for his research.
Edit to add: Looking at that repo, one thing I like (but others may find infuriating idk) is that where in the text he leaves certain proofs as exercises for the reader, in the repo he turns those into “sorry”s, so you can fork the repo and have a go at proving those things in lean yourself.
If you have some proposition which you need to use as the basis of further work but you haven’t completed a formal proof of yet, in lean, you can just state the proposition with the proof being “sorry”. Lean will then proceed as though that proposition had been proved except that it will give you a warning saying that you have a sorry. For something to be proved in lean you have to have it done without any “sorry”s. https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tac...
iNic•1h ago
seanhunter•50m ago
So although lean4 is a programming language that people can use to write “normal” programs, when you use it as a proof assistant this is what you are doing - stating propositions and then using a combination of a (very extensive) library of previous results, your own ingenuity using the builtins of the language and (in my experience anyway) a bunch of brute force to instantiate the type thus proving the proposition.
gaogao•59m ago
Python and C though have enough nasal demons and undefined behavior that it's a huge pain to verify things about them, since some random other thread can drive by and modify memory in another thread.