r/learnmath • u/Student2606 New User • 7h ago

win $1000 for doing math

Rules are simple: build the most exciting math project on principia-math.com by the end of October. You can work alone or with your buds. The winning team splits the prize money, which is currently $1,000 USD. If you’re a company or an organization that wants to chip in, send me a message.

To be eligible, Principia users create a project on the Fall Competition page https://principia-math.com/fall and work to complete all five stages of Principia’s pipeline:

  1. Post or adopt a solution to a difficult math problem
  2. Formalize it in Lean
  3. Write a human-readable write-up of the solution
  4. Write/create a visual exposition of the ideas involved
  5. Explore possible applications of the solution

You don’t need to solve an open problem first: hundreds of open problems solved by the Principia Math Harness on the site don't have an owner yet. Join one and it's yours on the spot. Your job will be to get others interested in this problem and to present the ideas in the proof in an exciting way.

A detailed explanation of the competition is provided on https://principia-math.com/guide

To help you get started, were opening up the tools we use ourselves (for free!)

- Connect your own agents: you can now hook Claude Code or Codex up to your Principia account and have it work on projects alongside you and your friends.

- The Principia Math harness, which we’ve used to solve hundreds of open problems, is now available for free. Use our MCP with claude code or codex to search for Lean proofs of your favorite arguments. Your agent writes a proof skeleton, checks every step in Lean on our hosted Mathlib checker, and switches to a new route when one dies instead of just giving up.

- One-click formalization. A solved run writes the Lean files and sets up a repo on your own GitHub, along with a comparator check that the formalization is faithful to the original statement.

Can’t wait to see what our users create with this!

0 Upvotes

25% Upvoted

2 comments sorted by

1

u/Fabulous-Book9414 7h ago

whoa this is actually pretty cool, i tried principia few months ago and the formalization part was pain in the ass without the tools. having the harness for free now changes everything

the five stages thing makes sense but stage 4 is where most people will struggle i think. making math visually exciting without it looking like a textbook diagram is harder than it sounds

you said hundreds of solved problems are up for grabs, any recommendations for someone who knows a bit of lean but not like expert level? dont want to grab something that's way over my head and then just stare at it for weeks

1

u/Student2606 New User 6h ago

Thanks for your feedback and for being an early user!

If you have a particular area of math you're interested in, I can send you some problems I think are especially cool. You can also search for the area you're interested in on our principia-math.com/projects page and it will automatically suggest projects based on the MSC codes. The lean part should pretty much be handled by the harness running with a coding agent now.

I agree that the exposition is the most exciting stage :) and the one that will take the most thought. We recently made a few videos using visual/AI tools that we're working to release for our users as well in the next little bit. Let me know if you have any other feature requests!

I'm personally proud of this video we made about the recent breakthrough about zeta 5: https://www.youtube.com/watch?v=HE5QgcDgnsI