51–60 of 73 posts
For software projects it seemed very approachable, even for a complete newbie like me. Probably not for Math though.
Earlier quoted context omitted.
This is horseshit. Mathlib3 and mathlib4 all existed prior to LLMs. Unimath of Agda, mathematical components of Rocq, the list goes on. LLMs have done nothing for "making large scale mechanization viable." They have been viable. The only thing has changed is the perception of the random developer who never wanted to put the effort into learning what actually needed to be learned and are instead happy to spit our comp…
> LLMs have done nothing for "making large scale mechanization viable." I'm sorry, but this assertion is ridiculous. LLMs absolutely have radically simplified mechanization. Autoformalization of papers using LLM is orders of magnitude faster than doing it manually. To quote Ken Buzzard (of the Xena Project): https://xenaproject.wordpress.com/2026/07/20/human-mathemati... > [...] Sol had generated 1.2 million lines of…
Earlier quoted context omitted.
> LLMs have done nothing for "making large scale mechanization viable." I'm sorry, but this assertion is ridiculous. LLMs absolutely have radically simplified mechanization. Autoformalization of papers using LLM is orders of magnitude faster than doing it manually. To quote Ken Buzzard (of the Xena Project): https://xenaproject.wordpress.com/2026/07/20/human-mathemati... > [...] Sol had generated 1.2 million lines of…
What is absurd is evaluating something on the lines of code it produces. AI psychosis at work.
Anyway, this avalanche is going to come down on your head whether or not you believe in it. Have fun!
Earlier quoted context omitted.
I actually noticed after I posted that I should have said 'by individuals at pace not too different from writing down a standard prose proof' or something similar to address this point. Mathlib for instance is of course a phenomenal project, but it was written by a large amount of people over many years. Granted their goal was not so much speed as it was elegance, but by 'viable' I had in mind something that a resear…
> The content in Mathlib still falls very much short of being enough for formalizing much of the actual research being done in mathematics, but people are now autoformalizing non-trivial extensions on top of that, Formalising non-trivial extensions on top of the standard library is not hard. I could bash out an average textbook formalisation at about half reading speed. The hard part is making something elegant and g…
Earlier quoted context omitted.
My favorite minimalistic example of the Metamath base language (which higher level languages can compile down to), which, saved as, say, prop.mm can be verified with the verifier: $c wff $. $( we use this $constant as a type of formula (well formed formula) $) $c ( ) ! -> $. $( brackets, negation, implication $) $v A B C $. $( $variables to be used in formulas $) wa $f wff A $. $( $floating hypothesis "wa" which says…
Fair to say that perhaps isn't selling it as much as you may think. It looks like perl that has been written by someone who is in the process of having a stroke.
Earlier quoted context omitted.
Idris has pi and sigma types, dependent pattern matching, view patterns, totality checking, proof search, interactive case splitting, etc, etc. It is orders of magnitude better then Haskell where the best you can do is hacky bullshit with singletons, GADTs, and type families.
Sure, but what I'm saying is that still doesn't make it nice to use as a proof assistant. As you say, the UX isn't there, no matter how much more terse the type system is at certain things in native semantics. Idris is designed to express executable programs, it has a wildly different grain to it than Lean or any other system designed to be used as a general proof assistant from the ground up.
For those who found it interesting, perhaps you will also find this term enjoyable https://en.wikipedia.org/wiki/Kairos for its similarity.
It would also seem highly agent-able since verification is very modular in SPARK.
Earlier quoted context omitted.
There are other forms of logic? is intuitionistic logic as rigorous? fascinating edit: the link says it is a weakening. if it is weakened, how can you prove the same stuff? i am a bit confused but i can see how it is useful for smarter people than me!
> if it is weakened, how can you prove the same stuff? Sometimes, you can't. In particular, so-called "non-constructive" proofs don't work in intuitionistic logic. Some mathematicians like to work in intuitionistic logic: for philosophical reasons, pragmatic technical considerations, or just because they think it's interesting.
Classical logic doesn't bother with this; positive and negative statements are completely dual to one another, and this duality is elegant in its own way (as people who are committed to classical logic will readily point out), but one needs linear logic in order to combine it with an awareness of constructive statements.