Collaborations looking for volunteers

Stream: new members

[Gerardo Jose Suarez]

I had known what lean is for about a year, but it never caught my interest until recently when I saw a popular science video on the busy beaver problem though I understand that Coq and not lean was used, I decided to come to this zulip because of a talk I saw on youtube with Terrence tao talking about proof asistants, I am a physicist by training (alreay checking some cool sutff out in the natural sciences channel), but will lkely not get into this, unless I see a reason and a supporting community to get some interaction, I was wondering if you guys know of anything like the busy beaver challenge where people are looking for volunteers to proof small sections of a bigger problem, or anything related where one can volunteer some time working on a problem that uses these
tools

[suhr]

Maybe porting (copying statements and doing proofs yourself) some code from Coq to Lean would be a good exercise.

[Gerardo Jose Suarez]

suhr said:

Maybe porting (copying statements and doing proofs yourself) some code from Coq to Lean would be a good exercise.

Indeed it is a good exercise, the reason I'm looking for such a volunteer task, is to have a goal to work on instead of just learning for the sake of learning, of course I would need to learn by doing this sort of stuff before, for now I'm just checking to see what the possibilities to use it are ( in this sort of online collaboration )

[Maja Kądziołka]

often such things are announced in various proof assistant discussion forums like this one. one high-profile one that comes to mind is the Fermat's Last Theorem project, though obviously that requires quite a bit of mathematics knowledge to contribute to.

in the case of the Busy Beaver project, it is a bit unusual in that the actual formal proof is not the area that needed many hands to complete the work – it's not a typical collection of interlinked lemmas that contribute to more and more understanding of a mathematical object, but rather a software program engineered to be relatively easy to prove correct. as such it's not a good source of lemma-sized TODOs

the aspect in which the Busy Beaver project was much more collaborative is actually finding the proof in the first place.

the way I found the project is that I was looking for a fun project to do in Coq, and I remembered the busy beaver function, which felt like it would have the type of theory around it that I would consider neat and approachable

[Maja Kądziołka]

so, I would say that a good way of finding a project to contribute would be: find a piece of math that interests you and go from there

[Kevin Buzzard]

Did you ask in #PhysLean ?

[Gerardo Jose Suarez]

You're absolutely right, that's always the best way to go! I was just thinking that this sort of busy beaver collaboration was popular, and was looking for something that I find interesting but at the same time had some people interested in it so that I could ask the community about the problem, get help I get stuck, etc ... I was sort of hoping there would be many people looking for counter examples of conjectures, or something like that when contributing would be easy

[Gerardo Jose Suarez]

Kevin Buzzard said:

Did you ask in #PhysLean ?

I didn't but found a course on youtube mentioned on the channel which I just started to take :), probably will go there after it :)

[Michał Mrugała]

There is also the Toric project if that’s up your alley