Proofs, personalities, and machines collide—intriguingly—at the uneasy intersection of mathematics and computer science.
How the labor-intensive process of proving mathematical theorems was transformed by computational tools.
Journalist Hartnett examines how Lean, an open-source computer program for validating mathematical proofs, emerged from a small, loosely organized group of collaborators pressing mathematics toward new thinking. In 1998, mathematician Tom Hales solved the Kepler conjecture, a notoriously difficult problem articulated by Johannes Kepler in 1611. Hales’ solution relied on inventive computational techniques, but when submitted to a leading journal, reviewers—unfamiliar with such methods—took years before concluding they could not validate it. As Hartnett observes, some traditional mathematicians relied on covering “blackboards with rows of chalky equations, while others fill reams of scrap paper filled with attempts to find arguments that generate a proof,” distrusting machines to certify results. Familiarity with mathematical terms is helpful while Hartnett delivers a largely accessible account, invoking concepts such as formal proofs and interactive theorem provers (ITPs). Central figure Leo de Moura of Microsoft Research leads the development of Lean by a global community of volunteers. Colorful high-profile characters include mathematicians Terry Tao, Jeremy Avigad, Kevin Buzzard, and Peter Scholze. In one pivotal episode, Scholze, a traditionalist who tested proofs in his mind but—“due to the complexity of the proof, and how significantly he thought it could change mathematics, due to all the beer he had had the night before his final breakthrough”—asked whether Lean could verify the proof. Lean’s successful verification marked a turning point in the program’s acceptance, energizing collaborators to continue enlarging “the scope of mathematical knowledge that could be verified by machines.” Especially for math-curious readers, programmers, and those following AI trends, de Moura’s “truth machine” is a fascinating example of how cultural clashes and creativity can create new paradigms.
Proofs, personalities, and machines collide—intriguingly—at the uneasy intersection of mathematics and computer science.Pub Date: June 9, 2026
ISBN: 9780374620059
Page Count: 288
Publisher: Quanta
Review Posted Online: Feb. 16, 2026
Kirkus Reviews Issue: March 15, 2026
Yes: it's high time for a de-romanticized, de-mythified, close-up retelling of the U.S. Space Program's launching—the inside story of those first seven astronauts.
But no: jazzy, jivey, exclamation-pointed, italicized Tom Wolfe "Mr. Overkill" hasn't really got the fight stuff for the job. Admittedly, he covers all the ground. He begins with the competitive, macho world of test pilots from which the astronauts came (thus being grossly overqualified to just sit in a controlled capsule); he follows the choosing of the Seven, the preparations for space flight, the flights themselves, the feelings of the wives; and he presents the breathless press coverage, the sudden celebrity, the glorification. He even throws in some of the technology. But instead of replacing the heroic standard version with the ring of truth, Wolfe merely offers an alternative myth: a surreal, satiric, often cartoony Wolfe-arama that, especially since there isn't a bit of documentation along the way, has one constantly wondering if anything really happened the way Wolfe tells it. His astronauts (referred to as "the brethren" or "The True Brothers") are obsessed with having the "right stuff" that certain blend of guts and smarts that spells pilot success. The Press is a ravenous fool, always referred to as "the eternal Victorian Gent": when Walter Cronkite's voice breaks while reporting a possible astronaut death, "There was the Press the Genteel Gent, coming up with the appropriate emotion. . . live. . . with no prompting whatsoever!" And, most off-puttingly, Wolfe presumes to enter the minds of one and all: he's with near-drowing Gus Grissom ("Cox. . . That face up there!—it's Cox. . . Cox knew how to get people out of here! . . . Cox! . . ."); he's with Betty Grissom angry about not staying at Holiday Inn ("Now. . . they truly owed her"); and, in a crude hatchet-job, he's with John Glenn furious at Al Shepard's being chosen for the first flight, pontificating to the others about their licentious behavior, or holding onto his self-image during his flight ("Oh, yes! I've been here before! And I am immune! I don't get into corners I can't get out of! . . . The Presbyterian Pilot was not about to foul up. His pipeline to dear Lord could not be clearer"). Certainly there's much here that Wolfe is quite right about, much that people will be interested in hearing: the P-R whitewash of Grissom's foul-up, the Life magazine excesses, the inter-astronaut tensions. And, for those who want to give Wolfe the benefit of the doubt throughout, there are emotional reconstructions that are juicily shrill.
But most readers outside the slick urban Wolfe orbit will find credibility fatally undermined by the self-indulgent digressions, the stylistic excesses, and the broadly satiric, anti-All-American stance; and, though The Right Stuff has enough energy, sass, and dirt to attract an audience, it mostly suggests that until Wolfe can put his subject first and his preening writing-persona second, he probably won't be a convincing chronicler of anything much weightier than radical chic.
Pub Date: Sept. 24, 1979
ISBN: 0312427565
Page Count: 370
Publisher: Farrar, Straus and Giroux
Review Posted Online: Oct. 13, 2011
Kirkus Reviews Issue: Sept. 1, 1979
BOOK TO SCREEN
A quirky wonder of a book.
A Peabody Award–winning NPR science reporter chronicles the life of a turn-of-the-century scientist and how her quest led to significant revelations about the meaning of order, chaos, and her own existence.
Miller began doing research on David Starr Jordan (1851-1931) to understand how he had managed to carry on after the 1906 San Francisco earthquake destroyed his work. A taxonomist who is credited with discovering “a full fifth of fish known to man in his day,” Jordan had amassed an unparalleled collection of ichthyological specimens. Gathering up all the fish he could save, Jordan sewed the nameplates that had been on the destroyed jars directly onto the fish. His perseverance intrigued the author, who also discusses the struggles she underwent after her affair with a woman ended a heterosexual relationship. Born into an upstate New York farm family, Jordan attended Cornell and then became an itinerant scholar and field researcher until he landed at Indiana University, where his first ichthyological collection was destroyed by lightning. In between this catastrophe and others involving family members’ deaths, he reconstructed his collection. Later, he was appointed as the founding president of Stanford, where he evolved into a Machiavellian figure who trampled on colleagues and sang the praises of eugenics. Miller concludes that Jordan displayed the characteristics of someone who relied on “positive illusions” to rebound from disaster and that his stand on eugenics came from a belief in “a divine hierarchy from bacteria to humans that point[ed]…toward better.” Considering recent research that negates biological hierarchies, the author then suggests that Jordan’s beloved taxonomic category—fish—does not exist. Part biography, part science report, and part meditation on how the chaos that caused Miller’s existential misery could also bring self-acceptance and a loving wife, this unique book is an ingenious celebration of diversity and the mysterious order that underlies all existence.
A quirky wonder of a book.Pub Date: April 14, 2020
ISBN: 978-1-5011-6027-1
Page Count: 224
Publisher: Simon & Schuster
Review Posted Online: Jan. 1, 2020
Kirkus Reviews Issue: Feb. 1, 2020
BOOK REVIEW
© Copyright 2026 Kirkus Media LLC. All Rights Reserved.
Follow
Popular in this Genre
We can’t wait for you to join Kirkus!
It’s free and takes less than 10 seconds!
Already have an account? Log in.
OR
Sign in with GoogleTrouble signing in? Retrieve credentials.
Welcome Back!
OR
Sign in with GoogleTrouble signing in? Retrieve credentials.
