[ldjkfkdsjnv]

You are talking about current capabilities versus what is probably possible. Sure, its not possible to write proofs with an LLM right now.

Somewhere inside openai is a reinforcement learning loop that looks like:

current_code = read(code_base_from_file.txt)

modify_prompt = "some prompt to modify code with expected outcome"

result = model.run(modify_prompt, current_code)

if check(result):

    provide_positive_feedback(model)

else:

    provide_negative_feedback(model)

and its clear that not only does this work, it maybe the future of what unravels software engineering.

the current models are being trained for coding, but theres no reason this couldnt be tried for other domains, like pure math.

[wizzwizz4]

It's not possible to write (usefully novel) proofs with an LLM, but we have other algorithms that can do that. Perhaps a reinforcement learning component could improve upon the search strategy in some way, but there's no compelling reason to use a predictive text model. (There's not even good reason to believe that naïve reinforcement learning would improve the mathematical ability of a system: RL says "that was good: do more of that", and mathematics is about discovery: thinking thoughts that nobody has ever thought before.)

[cycrutchfield]

Wow, so easy. Why didn’t anybody think of that before? How shall I inscribe your Fields Medal, sir?