logoalt Hacker News

yorwbatoday at 1:53 PM0 repliesview on HN

They use the properties of Wilkie's counterexample to restrict the search space. So you can't just pick arbitrary identities that hold over the positive integers and repeat the process until you've found a smaller model.