[maxwells-daemon]

I work at Harmonic, the company behind Aristotle.

To clear up a few misconceptions:

- Aristotle uses modern AI techniques heavily, including language modeling.

- Aristotle can be guided by an informal (English) proof. If the proof is correct, Aristotle has a good chance at translating it into Lean (which is a strong vote of confidence that your English proof is solid). I believe that's what happened here.

- Once a proof is formalized into Lean (assuming you have formalized the statement correctly), there is no doubt that the proof is correct. This is the core of our approach: you can do a lot of (AI-driven) search, and once you find the answer you are certain it's correct no matter how complex the solution is.

Happy to answer any questions!

[aidenn0]

How do you verify that the AI translation to Lean is a correct formalization of the problem? In other fields, generative AI is very good at making up plausible sounding lies, so I'm wondering how likely that is for this usage.

[sibrahim]

That's what's covered by the "assuming you have formalized the statement correctly" parenthetical.

Given a formal statement of what you want, Lean can validate that the steps in a (tedious) machine-readable purported proof are valid and imply the result from accepted axioms. This is not AI, but a tiny, well reviewed kernel that only accepts correct formal logic arguments.

So, if you have a formal statement that you've verified to represent what you are interested in by some other means, Lean can tell you whether the proof created by genAI is correct. Basically, there is a nigh infallible checker that won't accept incorrect hallucinations.

[mjevans]

I think the question is, how can humans have verification that the problem statement was correctly encoded into that Lean specification?

[ndriscoll]

The problem statement is apparently

> Let C>0 and ϵ>0 be sufficiently small. Are there infinitely many integers a,b,n with a≥ϵn and b≥ϵn such that a!b!∣n!(a+b−n)! and a+b>n+Clogn?

Which seems like it's the type of thing you give as a homework problem to state formally in an intro class.

[Jweb_Guru]

Yeah people dramatically overestimate the difficulty of getting one's definitions correct for most problems, especially when you are doing an end to end proof rather than just axiomatizing some system. They are still worth looking at carefully, especially for AI-generated proofs where you don't get the immediate feedback that you do as a human when something you expect to be hard goes through easily, but contrary to what seems to be popular belief here they are generally much easier to verify than the corresponding proof (in the case of formally verified software, the corresponding analogy is verifying that the spec is what you want vs. verifying that the program matches the spec; the former is generally much easier).

[oh_my_goodness]

Everyone has a different perspective, based on their math background. From the OP's perspective, the formalization of this problem statement was apparently worth talking about. On the other hand, for you it's just a homework problem that belongs in an intro class.

Let's just be generous and try to accept these differences.

[ndriscoll]

My comment was exactly about the required math background though. Anyone who's completed an intro to proof class would find that kind of statement easy to formalize because they would have had to write similar statements for homework. That provides some context: everyone who's interested in computer theorem provers probably has some experience with proofs, so formalizing that statement should be easy for them. i.e. (for this kind of problem) it's not really "the hard part" for people who are seriously working on this stuff.

[ccppurcell]

Are you an expert? Not gatekeeping here but I have no intuition for what is easy or hard to formalise. A lot of very simply stated graph theoretical results are apparently extremely hard to formalise.

[impendia]

> Are you an expert?

I can't speak for ndriscoll, but I am a university math professor with extensive experience teaching these sorts of topics, and I agree with their comment in full.

You are right that some (other) statements are harder to formalize than they look. The Four Color Theorem from graph theory is an example. Generally speaking, discrete math, inequalities, for all/there exists, etc. are all easy to formalize. Anything involving geometry or topology is liable to be harder. For example, the Jordan curve theorem states that "any plane simple closed curve divides the plane into two regions, the interior and the exterior". As anyone who has slogged through an intro topology book knows, statements like this take more work to make precise (and still more to prove).

[codeflo]

> apparently

When someone takes the time to explain undergrad-level concepts in a comment, responding with "are you an expert?" is a level of skepticism that's bordering on hostile. The person you're responding to is correct, it's rare that the theorem statement itself is particularly hard to formalize. Whatever you read likely refers to the difficulty of formalizing a proof.

[tetha]

As the sibling comment says, in my experience, the difficulty of formalizing the problem varies greatly between different areas. Probability theory is another notorious field in which modelling a problem correctly can be very subtle and difficult.

On the other hand, many problems in number theory and discrete structures tend to be rather simple to formalize. If you want to take your own look at that, I'd recommend to check out the lean games[1]. I'd say after the natural numbers game, you most likely know enough lean to write that problem down in lean with the "sufficiently small" being the trickiest part.

1: https://adam.math.hhu.de/

[dooglius]

I think you may be confusing specification of the problem and the formalization of the proof.

[schrodinger]

Voters: please reconsider your ups and downs. I think the “Are you an expert” question triggered a lot of downvotes when it was in fact asked in good faith to judge the person’s perspective of easy and hard.

[johncolanduoni]

They can read the statement, and the definitions that the statement references. If everything it references is in a well-tread part of the Lean library, you can have pretty high confidence in a few minutes of going over the syntax.

[saghm]

Isn't that kind of a general problem with proofs, even when they're written by humans? There's nothing stopping someone from accidentally writing their own Lean proof that has slightly different semantics than an English version of the same proof, or even for their English proof to subtly miss something important or make an incorrect logical leap. This seems like a bit of a double standard, although maybe there's nuance here I'm missing.

[teiferer]

One nuance you are missing is that the discussion is about formalizing the statement (the theorem), not the proof. The latter is what the article is about, but that doesn't suffice if you can't trust that the statement is also correctly formalized.

These are the two main problems:

1. Formalizing a theorem.

2. Finding a formal proof.

Part 2 is where AI could help as proof search is full of heuristics. That's also how humans find proofs and is one of the main skills of a mathematician. The formal proof can then be machine checked with well known and mature techniques not involving AI.

Part 1 is the part that's missing and will always be hard. It's also the issue with formal verification of programs for which correctness criteria are often very complex and it's easy to mess up the formalization, so that even if you trust the proof, you can't trust that it proves the right thing.

[digikata]

To borrow some definitions from Systems engineering for verification and validation, this question is one of validation. Verification is performed by Lean and spec syntax and logic enforcement. But Validation is a question of is if the Lean spec encodes a true representation of the problem statement (was the right thing specced). Validation at highest levels is probably an irreplaceable human activity.

Also, on the verification side - there could also be a window of failure that Lean itself has a hidden bug in it too. And with automated systems that seek correctness, it is slightly elevated that some missed crack of a bug becomes exploited in the dev-check-dev loop run by the AI.

[mrtesthah]

They probably need to be able to read and understand the lean language.

[aidenn0]

I can read and understand e.g. Python, but I have seen subtle bugs that were hard to spot in code generated by AI. At least the last time I tried coding agents (mid 2025), it was often easier to write the code myself then play "spot the bug" with whatever was generated. I don't know anything about Lean, so I was wondering if there were similar pitfalls here.

[mkehrt]

In this case the human written statement of the theorem is small. Can there be bugs? Absolutely! But it's essentially a few lines of code worth of thinking.

The lean proof checker then checks to make sure the proof actually proves the statement.

In this case an AI is generating the proof, but if it "compiles" it's correct. The only thing humans need to check is the statement to be proven.

(I don't know anything about this project but I've played around with lean and used other proof checkers more sesrisously).

[saghm]

I don't disagree with you, but on the other hand, I feel the same way about code written by other humans, and that's not because they're necessarily worse at writing code than me, but because for code I've written myself, I've already spent time thinking about it, so I don't have to start from scratch when re-reading it. It's also not like I don't think I potentially write as many bugs as my coworkers either; it's just easier for me to catch my own up front as I'm coding than it is to catch theirs in code review. The two main differences are that I can have a more meaningful conversation with my coworkers about their approach, what bugs they might think are worth looking out for, etc. compared to an LLM (which in my experience will claim completely incorrect things about the code it wrote far more often than any engineer I've worked with even junior ones; the humans I've worked with have uniformly been able to report how confident they are in what they've produced being what they were tasked with without insane exaggerations), and that an LLM can produce a much higher volume of plausible-enough looking code in a given unit of time than most humans I've worked with. It's not obvious to me that these would be particularly severe problems in generating proofs though; unless the proof is so large that it would be infeasible to read through it in a reasonable amount of time, I would expect mathematicians to be able to make up for the lower quality conversations with the "author" by devoting more time to reading and thinking, or having someone else also read through the proof and talking through it with them. If anything, it's possible that the timeline for writing up a paper about the results might be better for some mathematicians than the equivalent amount of time most engineers have to spend reviewing code before the pressure to get it merged and move on to the next thing. (I'm aware that there is certainly pressure to get things published in academia, but I don't have firsthand experience, so I've tried to be intentional in how I've worded this to clarify that I want to avoid any assumptions about what the norms would be, but given the relatively wide range of time pressure that engineers might experience across the industry as a whole, I'd expect that at least some mathematicians might have some flexibility to spend extra time reading through an LLM-written proof, especially if it might be time they'd otherwise have to spend trying to come up with the proof themselves).

[Jaxan]

If you want to check the statement, you only have to read the type. The proof itself you don’t have to read at all

[bryanrasmussen]

As I understand it Lean is not a general purpose programming language, it is a DSL focused on formal logic verification. Bugs in a DSL are generally easier to identify and fix.

It seems one side of this argument desperately needs AI to have failed, and the other side is just saying that it probably worked but it is not as important as presented, that it is actually just a very cool working methodology going forward.

[threatofrain]

It’s far easier for Lean because the human has to read very little compared to generating whole programs.

[luckydata]

the same way you verify that any other program compiles? I don't understand the question tbh, it seems self evident.

[NetMageSCW]

Compiling isn’t sufficient because it doesn’t tell you if the program matches the specification. A program that always says the temperature is 80 F will compile but is a terrible solution to what is the temperature outside at this location right now.

[oh_my_goodness]

>That's what's covered by the "assuming you have formalized the statement correctly" parenthetical.

Sure. But it's fair to ask how to validate that assumption.

[fsmv]

Skilled humans must understand the problem and write the theorem statement.

[f1shy]

> This is not AI,

A little bit nitpicking, but according to books like AIMA that is indeed AI. In the first chapter even any control system is classified as AI.

Because of the reasons stated in the 1st chapter, I totally agree with the authors.

The whole system is AI. That part is a verifier in a chain of “suggestions/instict -> verifier” like used in neurosymbolic systems for automated driving, for example.

[exe34]

the argument here is that:

1. you write a proof in English that there is an infinite number of primes. 2. the llm writes 2+2=4 in lean. 3. lean confirms that this is correct and it's impossible that this proof is wrong.

[NetMageSCW]

You missed a whole section - a person creates a Lean formalization of #1 and Lean promptly says the AI proof is wrong because it doesn’t prove that formal problem statement.

The question is in the person (or AI) creating the formal problem statement - how do you know it represents the problem the proof is supposed to be for? And the answer is for people in the field, in this case, formalizing the problem and verifying the formalization is easy. It is like generating an public key versus factoring it.

[exe34]

I thought that's what I was trying to express between lines 1 and 2 above, but I may have failed to get it across. my understanding is that the danger is that the llm will create a proof that is correct but isn't about what the person thinks he's proving?

[heroprotagonist]

Soo, it can definitively tell you that 42 is correct Answer to the Ultimate Question of Life, The Universe, and Everything. It just can't tell you if you're asking the right question.

[Someone]

No, it can tell you that 42 is the answer to (some lean statement), but not what question that lean statement encodes.

[davidwritesbugs]

I recently learnt that Douglas Adams wrote code and the ultimate answer was '*' - 42 in ascii

[bee_rider]

How hard is it to go back to English, from Lean? Just as hard as going from English to Lean?

If it is easier to convert backwards, maybe the AI can at least describe what the equations mean…

[rurban]

Lean is doing logical AI, the classical AI part.

Aristotle is doing the matching AI part, the modern LLM approach, previously called fuzzy logic.

Both are AI.

[teiferer]

Calling Lean "AI" is quite a stretch. Though I'm also in the camp that dislikes the inflationary use of "AI" for LLMs, so I have sympathies for your viewpoint.

[baq]

Finding a path in a maze was AI once.

[chpatrick]

I think that definition is pretty obsolete for the last 20 years.

To me "AI" is machine learning, statistical algorithms trained on data. That's not true for Lean.

[svat]

It may help to look at this example concretely:

The natural-language statement of the problem is (from https://www.erdosproblems.com/728):

> Let C>0 and ϵ>0 be sufficiently small. Are there infinitely many integers a,b,n with a≥ϵn and b≥ϵn such that a!b!∣n!(a+b−n)! and a+b>n+Clogn?

The Lean-language statement of the problem (which can be done either by hand or by AI) is (from https://github.com/plby/lean-proofs/blob/f44d8c0e433ab285541...):

    ∀ᶠ ε : ℝ in [>] 0, ∀ C > (0 : ℝ), ∀ C' > C,
      ∃ a b n : ℕ,
        0 < n ∧
        ε * n < a ∧
        ε * n < b ∧
        a ! * b ! ∣ n ! * (a + b - n)! ∧
        a + b > n + C * log n ∧
        a + b < n + C' * log n

Yes on the one hand, one needs to know enough about Lean to be sure that this formulation matches what we intend, and isn't stating something trivial. But on the other hand, this is not as hard as finding an error on some obscure line of a long proof.

(There's also an older formulation at https://github.com/google-deepmind/formal-conjectures/blob/f... but the new one is more in the spirit of what was intended: see the discussion starting at https://www.erdosproblems.com/forum/thread/728#post-2196 which gives a clear picture, as of course does Tao's thread in the OP that summarizes this discussion.)

[kovek]

I'm wondering how do people come up with these mathematical challenges?

[mikhailfranco]

Live out of a suitcase, travel the world, hang out with a wide selection of excellent mathematicians, write joint papers with many of them, when you get bored or stuck, pack the suitcase and keep moving - for your whole life.

[maxwells-daemon]

For this reason, when we announce results on e.g. the IMO, we formalize the statements by hand and inspect the proofs carefully to ensure they capture the full spirit of the problem.

However, there are some good heuristics. If you expect a problem to be hard and the proof is very short, you've probably missed something!

[tomjen3]

Aren't the best proofs very short?

[j_maffe]

"Best" is subjective. Proofs can get very long especially for the harder ones mathematicians are tackling these days.

[bytesandbits]

no you don't

https://www.reddit.com/r/singularity/comments/1pv3nl3/commen...

[minitech]

That doesn’t look like a counterexample to “we formalize the statements by hand and inspect the proofs carefully to ensure they capture the full spirit of the problem”.

[maccam912]

To answer the question a different way, I think you are asking how we know the proof actually matches the description the human provided? And I'd say we can't know for sure, but the idea is that you can pretty concisely write and check yourself that the problem is accurate, i.e. "There are an infinite number of primes" or whatever, and then even if an LLM goes off and makes up a lean proof wildly different from your description, if lean says the proof is valid then you have proven the original statement. I guess in theory the actual proof could be way different than what you thought it would be, but ultimately all the logic will still check out.

[rtpg]

I feel like even outside of AI translation, formalization not capturing the spirit of what the informal description was provided is always a risk.

This is also a big risk when trying to prove code correctness: "prove this algo works" means you gotta define "works" along certain axes, and if you're very unlucky you might have a proof that exploits the uncertainty around a certain axis.

[jlouis]

The statement is something you provide. It's the search you can have the LLM do. If this works for math it will immediately make code way higher quality via the same tools.

[JacobAsmuth]

You read it yourself :)

If you and the AI agree on the translation of the problem, and lean agrees with the solution, then you're done.

[roenxi]

You're looking for the practical answer, but philosophically it isn't possible to translate an informal statement into a formal one 'correctly'. It is informal, ie, vaguely specified. The only certain questions are if the formal axioms and results are interesting which is independent of the informal formalisation and that can only be established by inspecting the the proof independently of the informal spec.

[wizzwizz4]

Philosophically, this is not true in general, but that's for trivial reasons: "how many integers greater than 7 are blue?" doesn't correspond to a formal question. It is absolutely true in many specific cases. Most problems posed by a mathematician will correspond to exactly one formal proposition, within the context of a given formal system. This problem is unusual, in that it was originally misspecified.

[red75prime]

I suppose there's no formally defined procedure that accepts a natural language statement and outputs either its formalization or "misspecified". And "absolutely true" means "the vast majority of mathematicians agree that there's only one formal proposition that corresponds to this statement".

[varjag]

I think you suppose wrong. A statement like "the area of the square whose side is the hypotenuse is equal to the sum of the areas of the squares on the other two sides" doesn't seam out of reach of an algorithmic procedure like a classical NLP.

[red75prime]

Sure, we can write a procedure that recognizes some formal grammar, which intersects with the natural language. Defining the formal grammar that fully captures the current natural language understanding of the mathematical community is a bit harder.

[xiphias2]

First congrats!

Sometimes when I'm using new LLMs I'm not sure if it’s a step forward or just benchmark hacking, but formalized math results always show that the progress is real and huge.

When do you think Harmonic will reach formalizing most (even hard) human written math?

I saw an interview with Christian Szegedy (your competitor I guess) that he believes it will be this year.

[maxwells-daemon]

Thank you! It depends on the topic. Some fields (algebra, number theory) are covered well by Lean's math library, and so I think we are already there; I recommend trying Aristotle for yourself to see how reliably it can formalize these theorems!

In other fields (topology, probability, linear algebra), many key definitions are not in Mathlib yet, so you will struggle to write down the theorem itself. (But in some cases, Aristotle can define the structure you are talking about on the fly!)

This is not an intrinsic limitations of Lean, it's just that nobody has taken the time to formalize much of those fields yet. We hope to dramatically accelerate this process by making it trivial to prove lemmas, which make up much of the work. For now, I still think humans should write the key definitions and statements of "central theorems" in a field, to ensure they are compatible with the rest of the library.

[zozbot234]

> ... But in some cases, Aristotle can define the structure you are talking about on the fly! ...

Do you have any plans to characterize these cases more fully, and perhaps propose your own contributions to mathlib itself on that basis?

[tachim]

There have been many contributions to mathlib from Aristotle already, it’s a major use case for our users

[pvillano]

Is anyone working on applying these techniques to formal verification of software?

My limited understanding of Rust is that it applies a fixed set of rules to guarantee memory safety. The rules are somewhat simple and limiting, for ease of understanding and implementation, but also because of undecidability.

Programmers run into situations where they know that their code won't cause memory errors, but it doesn't follow the rules. Wouldn't it be cool if something like Aristotle was integrated into the compiler? Any code for which a proof of correctness could be written would pass/compile, without having to add more and more rules

[maxwells-daemon]

We are! We very recently announced some results on formally proving the correctness of programs: https://harmonic.fun/news#blog-post-verina-bench-sota

Formal methods are cool because, by contrast to tools like the borrow checker, you can prove some very "nonlocal" properties: this system does not deadlock, or it makes progress at least every N steps, etc.

[vatsachak]

Does Aristotle produce TLA+ output?

For example can it read rust async code and prove that there are no deadlocks in TLA+, or some equivalent in Lean?

[zozbot234]

TLA+ is generally used to specify a "toy model" of some complex distributed system. It's not intended for end-to-end proof, for that you'd just use Coq/Rocq or Lean itself. Lean is certainly expressive enough, but you'll have to translate the time and non-determinism modalities of TLA+ as part of the Lean development.

[NetMageSCW]

How is “this system doesn’t deadlock” not the same as the halting problem?

[xjm]

Proving that a particular program terminates does not require deciding the halting problem on arbitrary programs (same for deadlock freedom)

[pvillano]

Deadlock is literally a halting problem.

We can't know for every possible program if it halts or not, but the complexity of programs we can determine is increasing as tools and techniques get better

[teiferer]

An issue with this approach is that it may not be robust. That is, you could run into a casr where a minor modification of your program is suddenly not provable anymore, even though it is still correct. The heuristic (AI or otherwise) has necessarily limits, and if your are close to the "edge" of its capabilities then a minor change could push it across.

If the proof is rooted in the programmer's understanding who can give proof hints to the prover then any modification of the program can then be accompanied with a modification of the hints, still allowing automatic proofs. But if the human has no clue then the automatic system can get stuck without the human having a chance to help it along.

[amelius]

The same is true for optimization. One small change and the compiler's optimizer doesn't know anymore how to optimize the code, and your code is now slow. And there is no way for a programmer to fix it except by rolling back their changes or by inspecting the assembly output.

[zozbot234]

Formal verification of program correctness is also (for obvious reasons) key to unlocking AI-driven synthesis (i.e. 'vibe' coding) of "correct" programs that will verifiably meet the given spec.

[tomjen3]

It will certainly help - but its an extremely high bar. Almost all formal verification of software today is "does this pass the typechecker"?.

Now this captures some errors, but it doesn't really capture high level ones (is this program guaranteed to not deadlock is a hard one), and it doesn't capture the one that is important for business purposes (does this do what the customer wants). That requirement is more important than correctness (vitness all the software that is described as "crap", but is nonetheless widely used).

I don't think this is a required key to unlocking vibe coding. That seems to be easy: does this provide business value? And there the answer seems roughly to be "yes".

[eru]

Not all aspects of a spec can be formally encoded. But even half-way houses are good.

Eg you can give the vague spec 'build me a todo list app', but you can still formally prove that everything your app does finishes, or even that it finishes in reasonable time.

[f1shy]

Yes. For sure we will never be able to 100% automate the whole SWE process. As you say, the first input is a human wish, and there comes the joke of the genie that always screw the wishes by leaving something obvious out, because not explicitly specified. Also I think at some point the halting problem will make some programs impossible to test. But it would so great, program in a loose syntax, but with more safety than Rust and Ada together

[eru]

> Also I think at some point the halting problem will make some programs impossible to test.

No, not at all. The halting problem isn't much of a problem here.

To elaborate: yes, it's pretty much impossible to decide whether an arbitrary programme will halt. But we aren't dealing with arbitrary programmes, you carefully have your agent craft programmes that are easy to prove correct.

There are languages available today whose type systems already only let you write terminating programmes. See eg https://news.ycombinator.com/item?id=32102203 the Dhall language. Or Agda or Lean itself (unless you specifically opt out via the 'partial' keyword. But it's trivial to check whether someone used 'partial'.)

If your agent write a programme that's not easy to prove to be terminating, you don't try harder to prove. You just flag that as an error and have the agent try again.

Just like as a human code reviewer you reject Pull Requests that are too complicated to understand: you don't even bother figuring out whether they are technically correct or not.

[f1shy]

Thanks. I expressed it with doubt, because I assume there had to be some way around.

If I understood correctly, the halting problem states you cannot make a program to test any program. But you can do if you test a relatively small, possibly finite and well defined subset of programs, right?

[wslh]

This is the forst time I heard about Aristotle and find it very interesting. First question first: is it available for the general public? I don't know if this is the page to try it? [1]

Second, when you say language modeling support, it means that can better understand code representation (ASTs) or something else? I am just an AI user, not very knowledgeable in the field. My main interest is if it would be great for static analysis oriented to computer security (SAST).

[1] https://aristotle.ai/

[tachim]

Yes it’s available! https://aristotle.harmonic.fun/

[qnleigh]

> If the proof is correct, Aristotle has a good chance at translating it into Lean

How does this depend on the area of mathematics of the proof? I was under the impression that it was still difficult to formalize most research areas, even for a human. How close is Aristotle to this frontier?

[nateberkopec]

>assuming you have formalized the statement correctly

That's a pretty big assumption, though, isn't it? As we saw the Navier-Stokes psychosis episode over the New Year holiday, formalizing correctly really isn't guaranteed.

[bjt12345]

What occurs when this process is reversed - translate from lean to informal english, and does iterating this then help research better approaches toward writing proofs in human language?

[hannasm]

I had the same thought but unfortunately even if that translation is accurate it could still be bidirectional hallucinating and would not really be sufficient evidence...

It's another reformulation rather than a true proof. Now, instead of wanting a proof of a theorem, now we just need to prove that this proof is actually proving the theorem. The proof itself being so incomprehensible that it can't on its own be trusted, but if it can be shown that it can be trusted then the theorem must be true.

[uoaei]

You seem to be openly contradicting your company's PR and language. Your description very clearly describes the "AI" as a tool to translate relatively informal specifications into formal proof logic, but does not itself do the proving.

[jjmarr]

What are the benefits of Aristotle over a general-purpose coding assistant like Claude Code?

[maxwells-daemon]

Aristotle's output is formally verified in Lean, so you can run it for days on a hard problem and be assured that the answer, no matter how complex, is right without needing to manually check it.

Claude Code can write lean, but we do a heck of a lot of RL on theorem proving, so Aristotle winds up being much better at writing Lean than other coding agents are.

[jjmarr]

Seeing a task-specific model be consistently better at anything is extremely surprising given rapid innovation in foundation models.

Have you tried Aristotle on other, non-Lean tasks? Is it better at logical reasoning in general?

[runeblaze]

Is it though? There is a reason gpt has codex variants. RL on a specific task raises the performance on that task

[jjmarr]

Post-training doesn't transfer over when a new base model arrives so anyone who adopted a task-specific LLM gets burned when a new generational advance comes out.

[runeblaze]

Resouce-affording, if you are chasing the frontier of some more niche task you redo your training regime on the new-gen LLMs

[Davidzheng]

how strong is your internal informal LLM at theorem-proving before the formalization stage? or it's combined in a way so that is not measurable?

[pfdietz]

Do you have plans to apply this broadly to the historical math literature?

[maxwells-daemon]

Yes! I think that working with Mathlib is the best long term solution, because it's how people already collaborate on building out the formal "universe of mathematics." We want to speed that up, and hopefully we'll cover all of the common topics very soon!

[EE84M3i]

> there is no doubt that the proof is correct.

Do you have any links to reading about how often lean core has soundness bugs or mathlib has correctness bugs?

[nottorp]

So what did the "AI" actually do?

Translate an informal description of the proof into this Lean?

[dpe82]

TFA says ChatGPT wrote the informal description.

[101008]

Any chance Harmonic accept full remote employees? :)