Gauss from Math, Inc. has formalized the proof - g/math

Stop being the product.

Become the owner.

or

g/math

5mo

ago

public

$0

earned

0

reactions

Gauss from Math, Inc. has formalized the proof of Erdős Problem #1196 . The initial proof was 7.2K lines of Lean, done in ~5 hours. Subsequent golfing has compressed it down to 4K lines.

Github repo for the code:: https://github.com/math-inc/Erdos1196/tree/main

From Math, Inc. on 𝕏: https://x.com/mathematics\_inc/status/2044717899944960037 https://x.com/mathematics_inc/status/2044717899944960037
#science

tip

loved

laughed

shocked

sad

angry

not impressed

	earnings
	0 mlx total
	$0 total

	engagement
	0 views
	0 reactions

0 comments