sam_ezeh

This isn't correct. This is only true for first-order theories of the natural numbers using the axiom schema of induction. Second-order Peano arithmetic with the full axiom of induction has the natural numbers as its only model. This property is called "categoricity" and you can find the proof here [1] if you're interested

>This repository provides a framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning models using Lean 4

FV of AI systems is hard and this repo massively oversells itself. The Lean code itself is weird (AI generated?) and the "fairness" example proves that if a (linear) classifier always returns "yes" then the percentage of people classified as "yes" is the same across all demographics which isn't meaningful since this percentage is 100% for every possible group of people.

I was watching a video [1] the other day about the challenges FV faces for AI if it's something you're be interested in. I'm not really familiar with FV for neural networks and not sure what progress looks like in the field but I know ANSR [2] and TIAMAT [3] are doing related things

Related is the platonic representation hypothesis where models apparently converge to similar representations of relationships between data points.