The Mathlib Initative is hiring! www.renaissancephilanthropy.org/careers/math... (part-time contractor, helping to solve the "2000 PRs" issue, note the required qualifications) and www.renaissancephilanthropy.org/careers/devo... (full-time, solving distributed systems challenges). 14 Sept deadline.
Mathematics is also incomplete (assuming it's consistent) and that hasn't stopped lean from engaging with it at research level
@sciam.bsky.social gave me the opportunity to share some personal thoughts about the recently reported AI results from the #imo2025:
NSF announces funding for ICARM: the Institute for Computer-Aided Reasoning in Mathematics, based in Carnegie-Mellon . Amazing! Carnegie-Mellon press release here: www.cmu.edu/news/stories...
Accept submissions of explicitly unfinished ideas, theories, or speculative models to start discussion. Gets more finished with feedback from reviewers and/or readers.
Among continuous optimization problems, convex problems (with convex objectives and convex constraints) define a class that can be solved efficiently with a variety of algorithms and with arbitrary precision. This is not true more generally when the convexity assumption is removed (see this post). This of course does not mean that (1) nobody should attempt...
I am very happy to say that I have recently received a generous grant from the Astera Institute to set up a small group to work on automatic theorem proving, in the first instance for about three years after which we will take stock and see whether it is worth continuing. This will enable me […]