--- Log opened Mon Mar 21 00:00:32 2022
00:03 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
00:04 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
00:19 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
00:20 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
01:04 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
01:05 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
01:31 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
01:31 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
02:03 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
02:04 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
02:16 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
02:17 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
03:15 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
03:15 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
03:32 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
03:32 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
04:15 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
04:16 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
05:03 -!- ghost43_ [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
05:05 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Ping timeout: 240 seconds]
05:13 -!- ghost43_ [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
05:14 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
06:05 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
06:06 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
06:08 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
06:08 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
06:33 -!- halosghost [~halosghos@user/halosghost] has joined #secp256k1
07:02 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
07:03 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
07:30 -!- halosghost [~halosghos@user/halosghost] has quit [Quit: WeeChat 3.4.1]
08:00 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
08:01 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
08:16 -!- yakshaver [yakshaver@2600:3c00::f03c:92ff:fe8e:dce6] has quit [Quit: ZNC 1.7.2+deb3 - https://znc.in]
08:16 -!- yakshaver [~yakshaver@shindig.notmandatory.org] has joined #secp256k1
08:30 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
08:31 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
09:15 -!- halosghost [~halosghos@user/halosghost] has joined #secp256k1
09:31 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
09:32 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
10:00 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
10:01 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
10:26 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
10:27 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
10:32 < roconnor> I've proven secp256k1_u128_rshift correct for some definition of correct.
10:57 < sipa> Can you prove this definition of correct to be useful?
11:08 < roconnor> No, but I can provide some evidence by using the result in further proofs.
11:09 < sipa> Assuming self-referencial proofs are ok, that seems ok.
11:09 < roconnor> Even still I know of examples of bad definitions presisting quite far before being discovered.
11:10 < roconnor> There is a famous case where a prime number as defined as being divisible only by 1 and itself.  However the quantifier ranged over negative integers...
11:10 < roconnor> so according to this definition there were no prime numbers.
11:11 < sipa> -1 would be a prime number according to this definition
11:11 < roconnor> But many many facts about these "prime" numbers were (correctly) proven before someone tried to prove that 2 is prime and failed.
11:11 < roconnor> Maybe it was a number greater than 1 and only divisible by 1 and itself?
11:12 < roconnor> I guess I don't know what exactly the erronous definition was.
11:12 -!- ghost43_ [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
11:15 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Ping timeout: 240 seconds]
11:19 < sipa> I assume that a proof that there is no largest prime number could still work with this definition even!
11:21 < robot-dreams> I don't think the "usual" proof by contradiction works because "product of all primes + 1" might not be bigger than any of the existing primes anymore
11:22 -!- ghost43_ [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
11:22 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
11:23 < roconnor> In priciple my specification is easier to review than the C code, but it involves learning how to read these formal specifications, and there is room for them to be misread.
11:23 < sipa> Knowing that prime numbers are all >=1 , I think it's the case that the product of all prime numbers + 1 is larger than any given prime number. This is true even when there are no prime numbers.
11:25 < sipa> or in general, given any S for which for every element x in S holds that x>=1, "prod(S)+1 > y for every y in S" holds.
11:38 < real_or_random> at least "given a prime x, there's a prime y > x" also holds
11:38 < real_or_random> (when you forget the induction base...)
11:38 < sipa> right; i think that's equivalent to "there is no largest prime number"; it's not equivalent to "there is an infinite number of prime numbers".
11:39 < real_or_random> right
11:40 < real_or_random> reminds me of a quiz in one of our programming courses... the topic of the last lecture was some code doing stuff with polynomials, so the lecture had some basic facts about them
11:41 < real_or_random> including the fundamental theorem of algebra, in the form that a polynomial of degree n has at most n roots
11:42 < real_or_random> so the quiz hat this "true or false?" statement: "Every polynomial has a finite number of roots."
11:42 < sipa> Polynomials can't have infinite degree, right?
11:42 < robot-dreams> Trick question :)
11:42 < real_or_random> (the professor got it wrong the sample solution.)
11:42 < real_or_random> sipa: yeah, that was my thinking, too
11:42 < robot-dreams> p(x) = 0
11:43 < real_or_random> indeed...
11:43 < sipa> Nice.
11:44 < sipa> Then again, you were talking about codes. Those tend to use polynomials over finite fields/rings, for which this statement is trivially true :0
11:44 < real_or_random> ah no, I meant "source code"
11:44 < sipa> Ah, ok.
11:45 < real_or_random> it was common that a student pointed out some strange way to interpret the not fully formal question, so even the "wrong" answers was considered correct in the end. but here, they really switched to sample solution from "only true" to "only false"
11:45 < sipa> But the fundamental theorem of algebra is about complex numbers. Was this code operating actually on complex numbers?
11:45 < real_or_random> No, I think there are multiple theorems that people call the fundamental theorem
11:46 < real_or_random> that's why I gave the simple version here.
11:46 < real_or_random> I guess the lecture was about integer polynomials
11:46 < sipa> In any case, Wikipedia defines it as "every non-constant single-variable polynomial with complex coefficients has at least one complex root.".
11:47 < sipa> and equivalently, "every non-zero, single-variable, degree n polynomial with complex coefficients has, counted with multiplicity, exactly n complex roots"
11:47 < sipa> non-zero
11:47 < real_or_random> :)
11:55 < real_or_random> since we're anyway off-topic a little bit, let me leave this here https://www.youtube.com/watch?v=G7LJC9vJluU
12:00 < real_or_random> re primes: what's the definition of prime number people learned in school?
12:02 < sipa> @real_or_random re youtube: LOL
12:02 < real_or_random> the one I learned was "has exactly two divisors", and  I've never seen this definition somewhere else again
12:09 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
12:10 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
12:27 < robot-dreams> An integer p is prime if the ideal of Z generated by p is a prime ideal (jk)
12:32 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
12:33 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
13:10 < elichai2> real_or_random: I learned primes as x > 2 where only 1 and x divides x
13:15 < elichai2> I've also seen the fundamental theorem of algebra being quoted for "any 2 different degree d polynomials can have at most d shared solutions" and "any polynomial can be factored into linear(ie degree 1) polynomials as long as it is solvable"
13:15 < sipa> So 2 would not be a prime? ;)
13:16 < elichai2> sipa: argh you're right, x>=2, although I think as kids we would argue about is 2 a prime or not lol
13:16 < sipa> I certainly remember discussions about whether 1 is a prime, but not about 2.
13:17 < elichai2> oh yeah, that was not a mathmatical discussion, just kids having a hard time grasping the fact that an even number can be prime :)
13:19 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
13:19 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
13:20 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
13:20 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
13:49 -!- halosghost [~halosghos@user/halosghost] has quit [Quit: WeeChat 3.4.1]
14:03 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
14:04 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
14:13 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
14:13 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
14:15 < roconnor> I've proven secp256k1_u128_accum_u64 correct for some definition of correct. :)
14:20 < roconnor> I think I'll be working on secp256k1_umulh next.
15:06 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
15:07 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
15:10 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
15:10 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
16:13 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
16:13 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
16:14 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
16:15 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
17:04 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
17:06 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
17:19 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
17:20 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
18:18 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
18:19 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
18:19 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
18:19 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
19:00 -!- luke-jr [~luke-jr@user/luke-jr] has quit [Read error: Connection reset by peer]
19:03 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
19:04 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
19:04 -!- luke-jr [~luke-jr@user/luke-jr] has joined #secp256k1
19:07 -!- halosghost [~halosghos@user/halosghost] has joined #secp256k1
19:24 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
19:25 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
20:09 -!- luke-jr [~luke-jr@user/luke-jr] has quit [Read error: Connection reset by peer]
20:14 -!- luke-jr [~luke-jr@user/luke-jr] has joined #secp256k1
20:20 -!- luke-jr [~luke-jr@user/luke-jr] has quit [Ping timeout: 240 seconds]
20:20 -!- lukedashjr [~luke-jr@user/luke-jr] has joined #secp256k1
20:21 -!- lukedashjr is now known as luke-jr
20:25 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
20:26 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
20:40 -!- halosghost [~halosghos@user/halosghost] has quit [Quit: WeeChat 3.4.1]
21:01 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
21:02 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
21:24 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
21:24 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
22:03 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
22:04 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
22:14 -!- ghost43_ [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
22:17 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
23:04 -!- ghost43_ [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
23:05 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
23:05 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
23:09 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
--- Log closed Tue Mar 22 00:00:32 2022