CRM Exploratory Workshop

Since the seminal works of the MIT professors Gian-Carlo Rota in the 1960’s, and later Richard Stanley, combinatorics has become an important branch of modern mathematics where interplay of different areas arise. In particular, the Rota-Hero-Welsh’s Conjecture, proposed by Gian-Carlo Rota in the 1960s for graphs and later by Hero and Welsh for matroids, has long stood as one of the most tantalizing problems in combinatorics and algebraic geometry. It posited a deep connection between the combinatorial structure of matroids and the algebraic structure of projective varieties. Specifically, it conjectured that certain relations, now known as the Hodge Riemann relations, hold true for the intersection numbers of divisors on a projective variety defined by the matroid. Despite decades of effort from mathematicians around the world, the conjecture remained stubbornly unresolved, serving as a formidable challenge at the intersection of these two fields.

June Huh’s initial breakthrough came with his groundbreaking proof of Rota’s Conjecture [1], achieved through a novel synthesis of techniques from algebraic geometry, combinatorics, and homological algebra. His work unveiled the intricate connections between combinatorial objects such as matroids and algebraic varieties, providing a deep understanding of the underlying structures governing their intersection. Through meticulous analysis and innovative reasoning, Huh demonstrated that the Hodge Riemann relations indeed hold true, thereby resolving a decades-old mystery and opening up new avenues for exploration in combinatorial algebraic geometry.

Subsequently, Huh’s collaboration with Karim Adiprasito and Eric Katz [2] further illuminated the rich mathematical landscape that emerged from their initial breakthrough. Together, they delved into the study of positivity for matroids and polytopes, uncovering deep connections between combinatorial structures and algebraic geometry. Their research yielded not only elegant proofs of fundamental results but also novel mathematical objects that bridge the gap between discrete and continuous mathematics. Through their collaborative efforts, they uncovered new perspectives on toric varieties, matroid theory, and tropical geometry, among other areas.

On another direction it has become nowadays more and more popular formal logic systems used to formalize mathematical proofs. In this context, LEAN is getting more and more popular due to its is versatile, allowing for a wide range of applications and uses. This tool is growing day by day and we believe it would be good to show to a wide mathematical audience the state of the art of this tool.