Discussion: ICARM

Stream: general

[Matthew Ballard]

For questions and discussions about ICARM

[Kevin Buzzard]

Congratulations!

(see #announce > ICARM - A new NSF DMS institute @ 💬 for announcement)

[Floris van Doorn]

This is really great news! Congratulations, and thanks to the work you and others put into this.

[Matthew Ballard]

There are many people and organizations to thank for support including the Lean Community, the maintainers team particularly @Heather Macbeth , and the Lean FRO!

[Patrick Massot]

I was in Pittsburgh all of last year and I can tell everybody here that Jeremy Avigad put an insane amount of work into this. Of course many people worked on this, but this institute wouldn’t exist without Jeremy’s passion for helping other people getting a great environment to enjoy science in general and formal methods in particular.

[Jeremy Avigad]

If we tried to acknowledge all the people who helped make this happen, the list would be endless. The program directors at the NSF were heroic in finding a way to make this work in the current environment. We had business managers waking up in the middle of the night to work on paperwork. And the real work is just about to begin! We will lean on all of you in the months ahead.

[Alex Kontorovich]

Fantastic news, Congrats to all involved!!!

[Matthew Ballard]

To spoil the best part of our booth check out the animation @David Renshaw made for of the evolution of blueprint dependency graph for some familiar projects: https://youtu.be/tLHuVh7-G_8?si=iwxNAHuf-xtFrl8s

[David Renshaw]

I have published the code that I used to make these animations: https://github.com/icarm/animate-blueprint-depgraph

[Matthew Ballard]

ICARM's zulip instance at icarm.zulipchat.com is now live. We are currently hosting a discussion on the 1stproof.org project. One striking aspect to me is that right now the only seemingly-credible attempt outside of the major labs is from @Tomodovodoo who used Aristotle to formalize his solution. (Lots of other variables and taste here + things can change so please take any value judgement in the previous sentence with much salt.) Without Lean, I don't think that happens.

You can view the web-public discussion from anywhere. If you want to participate, please sign up at https://docs.google.com/forms/d/e/1FAIpQLSeY2HIkz4COUiBrA_Yp6X_mCQ7I43tEMtu4dA6putps2FDHJw/viewform

[Matthew Ballard]

I should add I am withholding any judgement on the accuracy of the formalization of the statement only because ICARM is the host. I encourage other experts to join and discuss