191–200 of 230 posts
He started learning lean4 with the help of GPT4 just at the start of the month: https://mathstodon.xyz/@tao/111208692505811257 Many of his mastodon posts this month have been about his learning progress. Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people
He started learning lean4 with the help of GPT4 just at the start of the month: https://mathstodon.xyz/@tao/111208692505811257 Many of his mastodon posts this month have been about his learning progress. Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people
They’re an easy 100x for the elite. Top engineers are now 10000x’ers.
Earlier quoted context omitted.
They’re an easy 100x for the elite. Top engineers are now 10000x’ers.
I don't think you realize what you are saying here. I agree that it is a large boost but 100x is just too ridiculous to take serious. Do you really believe an engineer can now finish in 20 hours what would have taking them a year before?
Earlier quoted context omitted.
I don't think you realize what you are saying here. I agree that it is a large boost but 100x is just too ridiculous to take serious. Do you really believe an engineer can now finish in 20 hours what would have taking them a year before?
As someone who uses ChatGPT4 pretty much nonstop all day (I have a monitor dedicated to it) - it's almost certainly a 10-20x in fields I have no knowledge of (writing in languages I've never used, dealing with OS/Kernel/Network constructs that are unfamiliar to me) - I can knock off in an hour what might have taken me a day or two previously - but I don't think I've ever had a task where I could say that I completed…
He started learning lean4 with the help of GPT4 just at the start of the month: https://mathstodon.xyz/@tao/111208692505811257 Many of his mastodon posts this month have been about his learning progress. Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people
They’re an easy 100x for the elite. Top engineers are now 10000x’ers.
Earlier quoted context omitted.
There are people doing this already. For Lean, an example is https://morph.so/blog/the-personal-ai-proof-engineer/
If I understand this correctly, they want to use an AI model for "autoformalization", which sounds like "using a language model to translate natural language proofs into Lean proofs". Which is cool but much less ambitious than the self-train system I described above. I guess AI technology isn't yet far enough to make such a proposal work.
If you have a denominator composed of “n - k - 1”, I hardly find it surprising that if n=3 and k=2 that you have a slight problem… Anyway, check out Idris[2], it’s cool for this sort of thing
I would be more impressed when some mathematician finds a more severe error in their proofs with the help of theorem provers (meaning a mistake in their own intuition).
He started learning lean4 with the help of GPT4 just at the start of the month: https://mathstodon.xyz/@tao/111208692505811257 Many of his mastodon posts this month have been about his learning progress. Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people
gpt4 is amazing, i rarely use google as as starting point for my programming related queries these days.
Earlier quoted context omitted.
Regarding usefulness: Lean is very nice to program in, if you care about pure functional languages; its FFI allows you to incorporate fast C routines very easily if pure Lean is not performant enough or lacks features. However, in some domains, Lean is within a decimal order of magnitude of (not hand-optimized) C; some benchmarks I hand-made recently impressed me. Regarding proving things about programs, no, it is no…
> the developers do not seem to consider it a core goal of Lean I guess it depends on who you ask. The original devs of Lean wanted to do "everything" (because that's how you start projects, I guess). Since then it has attracted a lot of mathematicians (especially those working on Mathlib, a library that aspires to formalize "all known math") who are happy to have "algorithm objects" and prove things about them witho…
Earlier quoted context omitted.
I'd say TLA+ is designed more for software people trying to design systems, write down specs, and reason about how the thing behaves dynamically. Lean is used mostly for writing down math proofs, and a lot less for software (although by the Curry–Howard correspondence, math proofs and programs have an equivalence, so the line is a little blurry). Lean has "mathlib", which is like a standard library of formally verifi…
Leo de Moura wants Lean 4 to be used for software verification too. A cool thing about Lean 4 is that it's also a programming language, using the same syntax as for proofs, making it easy to consider proving correctness properties of programs you write. Most of Lean 4 and its tactics are written in Lean 4 (though at this point almost none of this code has any associated proofs).
Do you have to actually prove a tactic work for it to be sound? A tactic will rewrite the program into a simplified program that will verified by a kernel; if the tactic wrongly expands something, the kernel will later reject the program. Only the itself kernel need to be verified for the whole thing to be sound.
Or am I missing something?