For people that know neither (like me 5 minutes ago):
>Lean4
> Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover.
> [...] is an Australian mathematician. He is a professor of mathematics at the University of California, Los Angeles (UCLA), where he holds the James and Carol Collins chair.
>Lean4
> Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover.
https://lean-lang.org/about/
> Terence Tao
> [...] is an Australian mathematician. He is a professor of mathematics at the University of California, Los Angeles (UCLA), where he holds the James and Carol Collins chair.
https://en.wikipedia.org/wiki/Terence_Tao