Developing code and theory concurrently

Stream: new members

[J. J. Issai (project started by GRP)]

A lot of chat on this server deals with formalization of existing mathematics, or a) look up the proof sketch in a journal (or your own notes), and then later b) attempt to formalize it in Lean.

I am formalizing an argument, and at the same time thinking of ways of improving the argument , leading to new (or improved) results. I want to know if this is happening to others (using Lean as a testbed for conjectures or proof attempts) where you try to formalize the (proof of a) result without knowing it in advance, but developing it as you go. Specifically, I want to know about successful workflows (where success does not have to be measured in terms of production rate of new results), and where one does b) and then a), or does b) and a) together.

Anyone have such examples to share?

[Kevin Buzzard]

I was annoyed about having to continually check that certain central algebras over the p-adic numbers were topological rings even though it was "obvious", so I asked about whether a module over a topological ring should inherit a canonical topology on mathoverflow, got an excellent answer from Will Sawin, coded it up into mathlib docs#IsModuleTopology and now use it all the time in my ongoing formalization of FLT.

[J. J. Issai (project started by GRP)]

@Kevin Buzzard : nice. This is close to the situation I have in mind. You saw a refactoring that would be useful if true (and it was "obviously" so), and then "looked at Will's notes" and then coded up the formalization. Granted this is in the middle of your project, so it looks like a) then b) then a) then b), so it could be considered a concurrent example.

My situation, (which is a work-in-progress) is that I am formalizing an argument, then I see an optimization which I tend to formalize, then I come up with a conjecture which I formalize, then I use Lean (with AI assistance if I must) to try to prove the conjecture before I work it out on paper. I am wondering if there are other examples like that. If so, how to work effectively to get and record results (which may be of interest but may never be Mathlib-worthy).

[Aaron Liu]

In the process of solving a birthday problem, I had a proof idea, but I did not check it rigorously. I was writing everything directly into Lean to confirm my arguments were valid, I didn't have a reference to follow. This lead to me having to at one point duplicate a definition in order to make the inequalities line up. And the whole time I wasn't completely convinced it would work, up until the moment I filled in the last sorry. Violeta Hernández has since cleaned up my proof and posted it on mathoverflow, and it is also available in the CGT repo as CGT#Surreal.birthday_toGame.

[J. J. Issai (project started by GRP)]

@Aaron Liu Cool! Did this lead to any more results or development beyond the birthday problem? (e.g., what is the smallest class of forms one could use to characterize a birthday?)

[Martin Dvořák]

J. J. Issai (project started by GRP) said:

I want to know if this is happening to others (using Lean as a testbed for conjectures or proof attempts) where you try to formalize the (proof of a) result without knowing it in advance, but developing it as you go.

Yes. Whenever possible, I try to develop the proof by looking at the Infoview only.

[Martin Dvořák]

J. J. Issai (project started by GRP) said:

Anyone have such examples to share?

The last thing I worked on in Lean is the following.

I took a proof of the Farkas-Bartl theorem
https://github.com/madvorak/duality/blob/2e7edafa9a5e9f087719b42cf54e3161fb02a85a/Duality/FarkasBartl.lean#L213
and I reworked it into a proof of the Fredholm alternative
https://github.com/madvorak/duality/blob/2e7edafa9a5e9f087719b42cf54e3161fb02a85a/Duality/Fredholm.lean#L180
without looking up its standard proof, without writing a single symbol on paper, only by examining the Infoview, judging what must be changed. It went really smoothly (though the resulting proof is not cleaned up yet; it is just a development branch, which isn't a part of my thesis or the paper that came out of it).

PS: I already had a proof of a very special case of the Fredholm alternative before, but I wanted to prove the Fredholm alternative in generality.

PPS: According to Wikipedia, what I proved is still not the most general version. Nevertheless, it is a huge step forward from the theorem I had before.

[Violeta Hernández]

J. J. Issai (project started by GRP) said:

Aaron Liu Cool! Did this lead to any more results or development beyond the birthday problem? (e.g., what is the smallest class of forms one could use to characterize a birthday?)

I don't think so... We're still missing a lot of results about surreal number birthdays, but we're working on them!

[Violeta Hernández]

On the topic of combinatorial game theory, we've also been concurrently formalizing and developing the theory of nimbers (CGT#Nimber). A friend of mine has an unpublished best upper bound for a 50 year old conjecture of Conway (finding the least algebraically closed nimber after ω^ω^ω), and one of the goals we're currently working on is to formalize her result. (And perhaps, in the meanwhile, find a full answer to this problem?)

[Violeta Hernández]

Lean has been particularly valuable in verifying arguments that I might have otherwise not had full faith in. And it's helped keep track of which hypotheses are needed where.