We develop an optimize-then-refine framework for the classical Heilbronn triangle problem that integrates global mixed-integer nonlinear programming with exact symbolic computation. A novel symmetry-breaking strategy, together with the exploitation of structural properties of determinants, yields a substantially stronger optimization model: for n=9, the problem can be solved to certified global optimality in 15 minutes on a standard desktop computer, improving upon the previously reported effort of about one day by more than an order of magnitude. Combining the numerical certificate with exact symbolic computation, we provide the first proof that the configuration discovered by Comellas and Yebra in 2002 for n=9 is globally optimal, and derive exact coordinates for all optimal configurations with n=5,…,9, confirming earlier best-known results and sometimes simplifying their presentation. An analysis of these configurations reveals structural patterns—notably the clustering of noncritical triangle areas around a small number of distinct values—which give rise to new research questions about the combinatorial geometry of extremal point sets. All configurations and code are publicly available to provide a reproducible foundation for further research.