The co-pilot is a large language model (LLM), the same kind of machine-learning system behind OpenAI’s ChatGPT and Google’s Gemini. While its training is different, it is also similar to the technology powering Google’s AlphaProof and AlphaGeometry 2—both of which generated complex mathematical proofs to a silver medal standard at this year’s International Mathematical Olympiad (IMO) for the world’s best high school students. And although LLMs can generate what is, in a technical sense, “bullshit,” a co-pilot’s erroneous suggestions are checked and rejected. In the case of the Caltech co-pilot, that’s thanks to the software in which the AI operates, called Lean, which uses rigorous mathematical logic to screen for valid statements.