 |
Post AvYrQr0hjAsjO1VF5s by [email protected] |
 |
More posts by [email protected] |
|
Post #AvYrQp4suf2NOPRYKe by [email protected] |
|
0 likes, 0 repeats |
|
|
|
Chat is this true? Is it really an open problem to prove "prime Fibonacci&… |
|
|
|
Post #AvYrQpV7L81MhliVDk by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@pigworker |
|
|
|
Post #AvYrQpnYEalZcwLDxA by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger Let's add it to https://github.com/google-deepmind/formal-conj… |
|
|
|
Post #AvYrQpudoERByvet0K by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching that is a great idea (rephrased to be the actual conjecture) |
|
|
|
Post #AvYrQpw3ixZW3KK1DM by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@pigworker I am nerd sniped because this feels like it shouldn't be hard, b… |
|
|
|
Post #AvYrQq2nJuxYODTOiG by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching I have to pick up my baby soon, but I can take a look tomorrow… |
|
|
|
Post #AvYrQqCMkKcErtx2dE by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching or I can just try tomorrow, but I am not as fluent in Lean as … |
|
|
|
Post #AvYrQqHgQYrx8ORHv6 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger Cool, this really should be a the perfect conjecture for people le… |
|
|
|
Post #AvYrQqNi49gpR5G6JU by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching OK I'll try tomorrow and if I have trouble I'll let yo… |
|
|
|
Post #AvYrQqQBuvftYmQ5BI by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@pigworker and you are the master of clever termination proofs |
|
|
|
Post #AvYrQqTjhkVhjm4uhs by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching I got started and I'm so lost on what types to use... Fib … |
|
|
|
Post #AvYrQqaTIhtk4fEICm by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger Perhaps something like```def FibonacciNumbers : Set ℕ := (fun n… |
|
|
|
Post #AvYrQqhur1qwRkiEoC by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger ok, not using "filter", but just "and":def Fib… |
|
|
|
Post #AvYrQqnwUcfokRX3Ca by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger or something likedef IsFibonacci (n : ℕ) := ∃ k, n = Nat.fib k… |
|
|
|
Post #AvYrQquK6tmH4EW99E by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching I'll put it together soon, going to try to mirror conventi… |
|
|
|
Post #AvYrQr0hjAsjO1VF5s by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching but that one is more natural to me for sure, standard sigma ty… |
|
|
|
Post #AvYrQr6jMlhbgiK3UG by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching I have this below (now with the spelling fixed). But I am in t… |
|
|
|
Post #AvYrQrEWtlwO4tyHdw by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching my ass can't spell Fibonacci lmao fixing that |
|
|
|
Post #AvYrQrLcTPc0QtHwh6 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching ok fixed the spelling, and used the "problem imports"… |
|
|
|
Post #AvYrQrSM4N02lmRKC0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching Here you go! Thanks for the motivation to actually properly in… |
|
|
|
Post #AvYrQrZncgxF8rvGnQ by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger A good place would be the "Wikipedia" dir inside FormalC… |
|
|
|
Post #AvYrR6vGZA2Sjn57q4 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MoritzFirsching ok, I'll put something together tomorrow then, though you … |
|
|
|
Post #AvYrR8nXar30YPTz4i by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger Fantastic, looking forward to the pull request, I hope I didn'… |
|
|
|
Post #AvYrRHFq9WRCmUmhIO by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger No I'm not. I'm the mistress of writing a different progra… |
|
|
|
Post #AvYrRHMZkTpF7Nw4nI by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@pigworker (my use of master was not gendered, sorry if unclear) I think it'… |
|
|
|
Post #AvYrRHTJLRDHSH5SIC by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@pigworker oh so it might just genuinely not terminate lol |
|
|
|
Post #AvYrRHZgxiJjm44YEq by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger We can make the stream of fibonacci numbers, productively, no trou… |
|
|
|
Post #AvYrRHfibJ8c4ktMdE by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@pigworker to me the vibes feel like it should be infinite but my vibes could b… |
|
|
|
Post #AvYrRHmSCGWePe2k88 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger @pigworker The number of people who correctly vibe number theory i… |
|
|
|
Post #AvYrRHspoXd6jR1q4m by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@JacquesC2 @pigworker well the only way to know is when it gets proven one way … |
|
|
|
Post #AvYrRHzDQojZ3E0w1Q by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@JacquesC2 @pigworker if @tao wants a challenge in Lean lol (but for real it is… |
|
|
|
Post #AvYrRYFOyPBjU3i5TM by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@TaliaRinger @pigworker It is not known whether there are an infinite number of… |
|
|
|
Post #AvYrRYLmagIBnqhBQ0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tavianator oh I'm an idiot so it might just genuinely *not* terminate (see… |
|
|
|
Post #AvYrRlJQOl8A0Igz32 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tavianator oh because it's printing all of them lmao |
