Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Lean4 helped Terence Tao discover a small bug in his recent paper

mathstodon.xyz

Post reply on HN
Print view View original

211–220 of 230 posts

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#211

Post by an_aparallel »

marshray wrote: post #187
mensetmanusman wrote: post #139

Earlier quoted context omitted.

I have found that good communicators that don’t code can quickly make functional automation. Interestingly, LLMs may end up contributing to more inequality if only the highly skilled can leverage them effectively.

My friend had never written anything more than an Excel formula a few months ago and now he's using GPT-4 to write very nontrivial Python applications and automate large parts of his job. I (having 30 years experience as a professional Software Developer^TM) am begging him to teach me his techniques. Now that you mention it, I met him and we became friends in large part due to his communications abilities.

5 months ago - a friend wrote me a python script and sent it to me...i couldnt get it to work. Used phind.com to explain what to do...it worked out my windows environment variables needed to be changed, told me how to structure a folder schema to place the src script...mindblowing stuff. And i have been using it - when it turn the same friend told me to write a similar script in python myself...it has been amazing to forego stackoverflow/google to get answers. When the GPT-4 model kicks in - my questions are answered with beautiful clarity...whether or not this technology "hallucinates" or not...without a doubt it's empowered me to learn to program. If it's helped me out of 50% of my ruts - i count that as overwhelmingly positive!

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#212

Post by heavenlyblue »

an_aparallel wrote: post #211
marshray wrote: post #187

Earlier quoted context omitted.

My friend had never written anything more than an Excel formula a few months ago and now he's using GPT-4 to write very nontrivial Python applications and automate large parts of his job. I (having 30 years experience as a professional Software Developer^TM) am begging him to teach me his techniques. Now that you mention it, I met him and we became friends in large part due to his communications abilities.

5 months ago - a friend wrote me a python script and sent it to me...i couldnt get it to work. Used phind.com to explain what to do...it worked out my windows environment variables needed to be changed, told me how to structure a folder schema to place the src script...mindblowing stuff. And i have been using it - when it turn the same friend told me to write a similar script in python myself...it has been amazing to…

I am not going to visit the website you just posted here unless you explain how the mechanism works, otherwise I will assume it's just crappy advertisement in this post.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#213

Post by hobs »

heavenlyblue wrote: post #212
an_aparallel wrote: post #211

Earlier quoted context omitted.

5 months ago - a friend wrote me a python script and sent it to me...i couldnt get it to work. Used phind.com to explain what to do...it worked out my windows environment variables needed to be changed, told me how to structure a folder schema to place the src script...mindblowing stuff. And i have been using it - when it turn the same friend told me to write a similar script in python myself...it has been amazing to…

I am not going to visit the website you just posted here unless you explain how the mechanism works, otherwise I will assume it's just crappy advertisement in this post.

Phind is just prompt engineering, as is anything sitting on top of anything OpenAI is building right now - if you are doing Q&A then maaaaybe it does some resource augmented generation as well (say, from Stack Overflow or other technical resources)

Phind is often recommended to me by programmers who find it produces "better" results than a naive GPT-4 session, but I don't know that anyone has done any real world testing.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#214

Post by hobs »

amelius wrote: post #209
pradn wrote: post #194

Earlier quoted context omitted.

The idea of the 10x programmer can mean 1) someone who produces a ton of code quickly 2) someone who can solve seemingly-intractable problems 3) someone who’s presence on a team improves everyone’s productivity quite a bit 4) someone who chooses technical decisions that save a ton of time down the line.

(1) is the generally accepted meaning. The others need different words.

Disagree, those are all valid interpretations, and depending on your experience you will have a vastly different understanding.

To me, the first one is the most basic and frankly, most silly definition of a 10x programmer - produces more code? really? Code sucks. Nobody needs more code, people need solutions. Solving a problem with no more code, or understanding it so a _tiny_ change solves all problems? Way better than adding code, actually much harder to synthesize and produce new results. Way more efficient.

Now can you remove things and solve the problem? Realize you can build an even more simple and generic system that solves your problem? Even more amazing.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#215

Post by amelius »

hobs wrote: post #214
amelius wrote: post #209

Earlier quoted context omitted.

(1) is the generally accepted meaning. The others need different words.

Disagree, those are all valid interpretations, and depending on your experience you will have a vastly different understanding. To me, the first one is the most basic and frankly, most silly definition of a 10x programmer - produces more code? really? Code sucks. Nobody needs more code, people need solutions. Solving a problem with no more code, or understanding it so a _tiny_ change solves all problems? Way better t…

> Nobody needs more code, people need solutions.

More code per unit of time, not necessarily more code in an absolute sense.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#216

Post by astrange »

heavenlyblue wrote: post #212
an_aparallel wrote: post #211

Earlier quoted context omitted.

5 months ago - a friend wrote me a python script and sent it to me...i couldnt get it to work. Used phind.com to explain what to do...it worked out my windows environment variables needed to be changed, told me how to structure a folder schema to place the src script...mindblowing stuff. And i have been using it - when it turn the same friend told me to write a similar script in python myself...it has been amazing to…

I am not going to visit the website you just posted here unless you explain how the mechanism works, otherwise I will assume it's just crappy advertisement in this post.

Nobody knows how LLMs work, much less LLMs behind an OpenAI server API, so that's a hard question.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#217

Post by melagonster »

heavenlyblue wrote: post #212
an_aparallel wrote: post #211

Earlier quoted context omitted.

5 months ago - a friend wrote me a python script and sent it to me...i couldnt get it to work. Used phind.com to explain what to do...it worked out my windows environment variables needed to be changed, told me how to structure a folder schema to place the src script...mindblowing stuff. And i have been using it - when it turn the same friend told me to write a similar script in python myself...it has been amazing to…

I am not going to visit the website you just posted here unless you explain how the mechanism works, otherwise I will assume it's just crappy advertisement in this post.

sorry, everyone is losing their job. we have no chances of living in future.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#218

Post by rey0927 »

oh_sigh wrote: post #179
rey0927 wrote: post #166

Earlier quoted context omitted.

I think you don't actually know about g-factor. basically what these so called 'intelligence tests' measure is the rate at which one can absorb information and apply it abstractly, how you can come up with solutions to problems by basically doing high-level abstractions, finding patterns and connecting dots, finding things that no one thought of or came to their mind. What this means is that even though he might not…

I'm familiar with g-factor. But why is it that the people who always score the highest on IQ tests contribute the most to math, and only a little bit to all the other subjects under the sun? Why aren't they also creating the greatest art, growing the greatest vegetables, and, I don't know, designing the greatest structural engineering designs in the world?

>greatest art

first, tell how one measures art

>greatest vegetables

If he does work in the field of animal/plant genetics I am hopeful he will discover great things and move the field forward

>structural engineering

again this is not what he does, and why he does math is.....i don't know what's his reason to do math, idk his motivations behind it but i do surely believe there are high-iq structural engineers out there of course they are how can you say there are none. greatest structural engineering designs made yet are actually made by geniuses or highly intelligent people you wouldn't expect a kid who fails high school to make those things do you?

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#219

Post by pfdietz »

kccqzy wrote: post #135
Genbox wrote: post #13

Earlier quoted context omitted.

Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model. C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checke…

Formal verification is often not the best tool for ensuring code correctness from an ROI perspective. Things like unit tests (including property based tests) and ensuring 100% code coverage often achieve adequate results with less effort.

If you can specify your program (or a part of it) well enough to prove it correct, you can also use that specification for property-based testing.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#220

Post by pfdietz »

cubefox wrote: post #44

I wonder whether we could combine formal proof checkers (like the Lean proof checker) with language models that generate synthetic conjecture-proof pairs in a formal language like Lean. The Lean proof checker could be used to automatically verify whether the synthetic proofs written by the language model are correct. This information could be used to provide an RL reward signal applied to the original language model,…

It would also be interesting to train these models on the entire math literature. One would want to use this to verify the math literature, translating the proofs there to checkable forms. Eventually, we would get a model that knows every theorem and every correct proof in the math literature.
Post reply on HN