A mathematician associated with set theory and the foundations of mathematics.

Marc Lackenby works in topology, geometry and group theory. His research includes knot theory, bounds on Reidemeister moves between knot diagrams, and hyperbolic geometry of link complements. These topics connect the geometric shape of three-dimensional spaces with the computational difficulty of recognizing and simplifying their descriptions.^[ref]

A mathematician whose 1926 work introduced a component-merging method for the minimum spanning tree problem, now called Borůvka's algorithm.^[ref]

John Pollard is a mathematician whose work in number theory includes Pollard's rho algorithm and Pollard's p-1 algorithm for integer factorization. His retrospective explains how collision ideas related to the birthday paradox lead to the rho method, and distinguishes its factorization and discrete logarithm applications.^[ref]

Homepage: sites.google.com/site/jmptidcott2/

A mathematician whose work includes Radon's theorem, Radon measures, the Radon-Nikodym theorem and the Radon transform.

A French mathematician whose work connected analysis, probability theory and mathematical physics. His 1837 study of probabilities of judicial decisions introduced the Poisson distribution. Its modern parameter $\lambda$ controls both the mean and variance of the count, making the law useful for modeling rare events.

His research on attractive forces and potential theory also helped shape the Poisson equation, relating the Laplacian of a potential to its source. His name appears in the Poisson bracket of Hamiltonian mechanics as well: the same biography reaches both statistical counts and the geometry of dynamical equations. ^[ref]

Portrait source. François-Séraphin Delpech, after Nicolas Eustache Maurin; existing crop hosted on Wikimedia Commons. The file cites the Smithsonian Libraries Scientific Identity source. Public-domain artwork; faithful reproduction, PD-Art / Public Domain Mark.

Øystein Ore worked in ring theory, Galois theory, lattice theory and graph theory. His work on noncommutative rings investigated when a ring can be embedded in a division ring, extending the idea of forming fractions beyond commutative arithmetic.

His later books also linked mathematical ideas with their history. The movement from algebraic structures to closure relations and graphs illustrates how an organizing mathematical viewpoint can lead into several different subjects.^[ref]

Harish-Chandra developed representation theory for Lie groups, especially infinite-dimensional representations of semisimple groups. His work connects continuous symmetries with operators on function spaces, extending the symmetry viewpoint familiar from quantum mechanics into deep questions in analysis and number theory.

He trained in theoretical physics before moving toward mathematics. The Institute for Advanced Study records his faculty affiliation from 1963 to 1983 and describes infinite-dimensional representations as a central theme of his work.^[ref]

Elizabeth Wong coauthored Sequential Quadratic Programming Methods by Philip E. Gill and Elizabeth Wong with Philip E. Gill. The review concerns constrained optimization, in which successive local quadratic problems determine steps and multiplier estimates.

Their work connects the design of optimization algorithms with the linear algebra needed to solve the local subproblems. The 2010 report's title page identifies the authors and institutional report number.^[ref]

Philip E. Gill works on numerical analysis, numerical linear algebra and scientific computation. With Elizabeth Wong, he authored Sequential Quadratic Programming Methods by Philip E. Gill and Elizabeth Wong, explaining how constrained nonlinear problems can be approached through successive quadratic models.

The connection with linear algebra is computationally important: solving the local constrained systems is part of making an optimization method reliable.^[ref]

British mathematician associated with numerical analysis and mathematical optimization, including Sℓ1QP.

Royal Society profile: royalsociety.org/people/roger-fletcher-11447/

A mathematician whose research includes mathematical optimization. The Dennis-Moré condition concerns superlinear convergence of quasi-Newton methods.

Homepage: www.cmor-faculty.rice.edu/~dennis/

A mathematician working on mathematical optimization algorithms and software. The Dennis-Moré condition concerns superlinear convergence of quasi-Newton methods.

Homepage: www.mcs.anl.gov/~more/

Henry Bessemer was an engineer associated with the Bessemer process, a method for converting molten pig iron toward steel using an air blast. His 1856 patent describes introducing air into molten iron so that reactions within the bath generate heat while changing its chemical composition.^[ref]

The important design insight is the coupling between chemical reaction, mixing and heating: the unwanted constituents become part of the source of energy for processing the material. The Bessemer process consequently illustrates how understanding a material's chemistry can change the scale and speed of manufacture. Obtaining a desired steel still requires control of the starting chemical composition and the final carbon content.

Identity and portraits: National Portrait Gallery, sitter biography and dated portraits.

A computer scientist whose work with Robert Tarjan includes splay trees and amortized analysis. His Carnegie Mellon University homepage identifies his full name and academic role.^[ref]

Computer scientist whose work includes algorithms, computational complexity theory and algorithmic game theory.

Official profile: www.cs.ox.ac.uk/people/paul.goldberg/

Armin Biere coauthored Symbolic Model Checking without BDDs by Armin Biere and others, which introduced a bounded model checking procedure for linear temporal logic using Boolean satisfiability. The method encodes a finite sequence of finite-state machine transitions as a propositional formula; a satisfying assignment can describe a path violating a requested property. The paper demonstrates how SAT solving can replace binary decision diagrams in this verification task.^[ref]

Alessandro Cimatti coauthored Symbolic Model Checking without BDDs by Armin Biere and others, which introduced a bounded model checking procedure for linear temporal logic using Boolean satisfiability. The method encodes a finite sequence of finite-state machine transitions as a propositional formula; a satisfying assignment can describe a path violating a requested property. The paper demonstrates how SAT solving can replace binary decision diagrams in this verification task.^[ref]

Edmund Clarke coauthored Symbolic Model Checking without BDDs by Armin Biere and others, which introduced a bounded model checking procedure for linear temporal logic using Boolean satisfiability. The method encodes a finite sequence of finite-state machine transitions as a propositional formula; a satisfying assignment can describe a path violating a requested property. The paper demonstrates how SAT solving can replace binary decision diagrams in this verification task.^[ref]

Yunshan Zhu coauthored Symbolic Model Checking without BDDs by Armin Biere and others, which introduced a bounded model checking procedure for linear temporal logic using Boolean satisfiability. The method encodes a finite sequence of finite-state machine transitions as a propositional formula; a satisfying assignment can describe a path violating a requested property. The paper demonstrates how SAT solving can replace binary decision diagrams in this verification task.^[ref]