@glynmoody They're using AI to produce a better verified math library than stealing existing code libraries or previously implementations? In what format? What are the reuse paths? Are they only formally verifying the algorithms, or will they formally verify all translations? e.g., symbolic (TeX, ???) to computer language (C, Python, ???) Do compilers/interpreters have to be vetted?