# Institute for Mathematical Sciences Programs & Activities

# ~ ABSTRACTS ~

**Maxima of Multivariate Data: Theory, Applications and
Algorithms**

*Hwang Hsien-Kuei, Academia Sinica, Taiwan*

Maximal elements of given multidimensional
point samples are naturally encountered in many scientific
disciplines and have been widely used under different names such
as noninferiority, Pareto optimality, admissibility, efficiency,
elite, skyline, etc. A survey will be given of the diverse
aspects of maxima in connection with probabilistic properties,
applications, and efficient algorithms for finding them.

**The Asymptotic Distribution and Berry-Esseen Bound of a
New Test for Independence in High Dimension**

*Shao Qi-Man, Hong Kong University of Science and Technology,
Hong Kong*

Let X1;X2; : : : ;Xn be a random sample from a p-dimensional population distribution. Assume that both p and n are large. To test whether the p-variates of the population are independent, Jiang (2004) uses the largest entry of the sample correlation matrix as a test statistic and the limiting distribution is the extreme distribution of type I. It is known that the rate of convergence to this type of extreme distribution is typically slow, of order of *O*(1/ log *n*).

In this talk we will introduce a newÂ test statistic which also has an extreme limiting distribution of type I but with a rate of convergence *O*( (log *n*)^{3 } / *n*^{ 1/2}). Other related problems will also be discussed. This talk is based on a joint work with W.D. Liu and Z.Y. Lin of Zhejiang University.

**An Introduction to Formal Proof**

*Thomas Hales, Mellon Professor, University of Pittsburgh*

A formal proof is a proof in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. The number of primitive inferences can run into the millions, even for a traditional proof of modest size. A number of noteworthy theorems have now been checked formally, including the four-color theorem, the Jordan curve theorem, and the prime number theorem (both the elementary and analytic proofs). This talk will describe the current stage of development of formal theorem proving technology. It will describe some research projects aimed at bringing formal theorem proving to every mathematician's desktop.

Brief Bio:

Thomas Hales is Mellon Professor of Mathematics at the University of Pittsburgh. He received his PhD from Princeton University under the supervision of Robert Langlands, and has held positions at MSRI Berkeley, Harvard University, University of Chicago and University of Michigan as well as membership at the Institute for Advanced Study, Princeton. He is best known for his (computer-aided) proof of the Kepler's conjecture, one of the oldest problems in discrete geometry, as well as the honeycomb conjecture. Hales advocates the formalization of mathematics to ensure rigor in an era where proofs are becoming increasingly complex and computers are becoming necessary to perform verification. He has received many prizes and honors for his work, including the Chauvenet Prize (2003), the R. E. Moore Prize (2004) the Robbins Prize (2007), the Lester Ford Prize (2008) and the Fulkerson Prize (2009). Hales has been invited to speak at many international meetings and conferences, including the Institute for Advanced Study, Public lecture series (1999), the National Academy of Science, Frontiers of Science Symposium (1999), the Joint Mathematical Meetings, AMS-MAA-SIAM (2000), the Euler Lecture at Berlin (2000), the International Congress of Mathematicians (2002), the Institute for Math and its Applications (IMA), Public Lecture Series (2005), the Institute for the Mathematical Sciences (PIMS) Distinguished Chair lectures (2006) and the Arnold Ross Lecture of the AMS (scheduled October 2010).