What do you mean "no new ground"? There is a very narrow, super constrained set of programs that we know how to formalize, some programs we kinda sorta hope we can, and absolutely everything else where we might not even bother. Check out what epic effort it took to prove 5th busy beaver. no visible abvances on collatz conjecture - and those are among simpliest things you can come up with! Any software that embeds similar behaviour is undecidable by construction. Which forces a rewrite to exclude such behaviour. Or, most likely, fabricating proof criteria that are unsound.

What is more likely, for AI agent that is trained with the goal of making user believe their problem is solved to solve exceedingly hard problem by developing novel theory, or to come up with plausible looking fake solution to the problem?

Fast fashion was mentioned as parallel to fast software — no incentives to lose profits.

New ground meaning quasi reimann, navier stokes, eth, yang mills existence, the strip mining of various fields openAI did recently, you know the stuff where it's triggering a crisis in mathematics around what the role of humans even is?

BB is proving things about all turning machines of a general size and it's unsolvable in general because 1. above a certain size you're encoding all the unsolved problems of mathematics 2. Halting problem.

BB and halting problem is also totally irrelevant here. We're talking about proving specific things about specific pieces of software, where we can change the software implementation to make the desired invariants easier to prove. Obviously there's the well known catch of just because you proved x doesn't mean that x being true implies whatever y behavior (security, class of bugs, etc) you're actually interested in but like, that's why we have standards committees and stuff. And the nice thing is there's sort of an evolutionary pressure when it comes to figuring out the right invariants for security in that anything you do will get aggressively stress tested by swarms of increasingly capable agents.

In terms of the alignment problem - the latter is possible and a risk but also you're talking about reward hacking like it's some gotcha instead of a thing people have been thinking about for decades and are spending hundreds billions of dollars on given at least the national security needs here and at worst the risk of catastrophic misalignment/rogue swarms. The huggingface hack is fresh in everyone's memory