Yes! I've been wondering if discovery fiction (in the sense of @michael_nielsen) and open-exposition problems (as introduced by Timothy Chow) might start to receive greater attention. It's also interesting to consider how AI might assist in these more subjective areas.

📢Stunning math & AI update "I still did not see how to prove this inequality, but I decided to try my luck giving it to ChatGPT Pro, which... gave me a duality-based proof..."—Terence Tao (3/23/26) How Fields medalist Tao used AI in his latest work: terrytao.wordpress.com/2026/…

The Institute for Computer-Aided Reasoning in Mathematics (ICARM), a new @NSF Mathematical Sciences Research Institute at Carnegie Mellon University @CarnegieMellon, is hosting a Summer School on Formalization in Lean @leanprover from July 7-18, 2026. Computational proof assistants now make it possible to develop global, digital mathematical libraries with theorems that are fully checked by computer. This summer school will introduce students to this technology and to the goals and benefits of formalized mathematics, including metaprogramming and autoformalization. By the end of the session, students will be in a position to formalize mathematics on their own, join the Lean community, and contribute to its mathematical library. School Structure The program interweaves short lectures with interactive tutorial sessions. The first week focuses on learning the Lean language and gaining comfort with the technology. During the second week, students will work on independent formalization projects in small groups with opportunities to share results and receive feedback. Optional tutorials on metaprogramming will also be available. Suggested Prerequisites - At least one undergraduate-level computer programming course - A mathematical area of interest for the student's formalization project For more information and to apply to participate, please visit: icarm.io/project/summer_scho…