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
A remarkably thorough and thoughtful case for the reconciliation between science and faith.
A duo of French mathematicians makes the scientific case for God in this nonfiction book.
Since its 2021 French-language publication in Paris, this work by Bolloré and Bonnassies has sold more than 400,000 copies. Now translated into English for the first time by West and Jones, the book offers a new introduction featuring endorsements from a range of scientists and religious leaders, including Nobel Prize-winning astronomers and Roman Catholic cardinals. This appeal to authority, both religious and scientific, distinguishes this volume from a genre of Christian apologetics that tends to reject, rather than embrace, scientific consensus. Central to the book’s argument is that contemporary scientific advancements have undone past emphases on materialist interpretations of the universe (and their parallel doubts of spirituality). According to the authors’ reasoned arguments, what now forms people’s present understanding of the universe—including quantum mechanics, relativity, and the Big Bang—puts “the question of the existence of a creator God back on the table,” given the underlying implications. Einstein’s theory of relativity, for instance, presupposes that if a cause exists behind the origin of the universe, then it must be atemporal, non-spatial, and immaterial. While the book’s contentions related to Christianity specifically, such as its belief in the “indisputable truths contained in the Bible,” may not be as convincing as its broader argument on how the idea of a creator God fits into contemporary scientific understanding, the volume nevertheless offers a refreshingly nuanced approach to the topic. From the work’s outset, the authors (academically trained in math and engineering) reject fundamentalist interpretations of creationism (such as claims that Earth is only 6,000 years old) as “fanciful beliefs” while challenging the philosophical underpinnings of a purely materialist understanding of the universe that may not fit into recent scientific paradigm shifts. Featuring over 500 pages and more than 600 research notes, this book strikes a balance between its academic foundations and an accessible writing style, complemented by dozens of photographs from various sources, diagrams, and charts.
A remarkably thorough and thoughtful case for the reconciliation between science and faith.Pub Date: Oct. 14, 2025
ISBN: 9789998782402
Page Count: 562
Publisher: N/A
Review Posted Online: Oct. 7, 2025
Review Program: Kirkus Indie
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
© 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.
