The Nineteenth Byte

Adám

12:00 AM

@cairdcoinheringaahing Thank you for that feedback.

New Posts

0

Q: Lean golf: Pascal vs. Fibonacci

The Pascal's triangle and the Fibonacci sequence have an interesting connection: Source: Math is Fun - Pascal's triangle Your job is to prove this property in Lean theorem prover (Lean 3 + mathlib). Shortest code in bytes wins. import data.nat.choose.basic import data.nat.fib import data.list.de...

New Loophole Proposal

12:18 AM

1

A: Loopholes that are forbidden by default

Sidestepping in a theorem-proving challenge A theorem-proving challenge is about proving a statement (= constructing a value of the given type) given in a specific host language (designed for theorem proving, most likely Lean or Coq). One problem with this is that the host language may have vario...

OldSandboxPosts

1:00 AM

Sandbox posts last active a week ago: How many values of this type?

AviFS

1:24 AM

@Bubbler Doesn't it make sense to expand the scope of the question to all langs capable of proving things. Of course, different ones begin with different assumptions, but supposedly competition is only between languages. So I can't see that it would take anything away from all the LotMers to allow other langs for the lean challenges.

lyxal

userinyerface.com

the first page requires a password with a cryllic character

the fools didn't count on me having many ways to quickly get unicode characters because golfing languages

AviFS

It doesn't seem different to me from allowing different langs to compete in code-golf. One could, of course, say some langs "import" more things for free. Eg C++ always has to import iostream, whereas Python gets print "for free." Isn't getting functions for free the same in spirit as other theorem-provers getting axioms for free?

Unrelated String

@Adám cube apple is great, parallel lines/ligature/quad all hurt my eyes, and the rest are nice

lyxal

I like cube apple the most

Unrelated String

@lyxal imagine not having a russian keyboard profile for typing flashcards

Adám

1:28 AM

@UnrelatedString @lyxal Thanks for the feedback.

Unrelated String

i feel like the two strongest points of the cube apple aside from the cube apple itself are the symbol-resembling font of the text and the way the cube is shaded; they give it a modern but distinctive feel

AviFS

@lyxal Is it possible to finish or does it keep cycling through captchas?

Oh... you have to select all of them facepalm

06:37

Bubbler

@AviFS It has been already discussed here (also see my comment there)

AviFS

@Bubbler Ah thanks, I hadn't realized; I'll check it out!

Wait, but the justification here is:

> I do think that any of these challenges would be significantly worsened by attempts to make them language agnostic. They would have to be very complex in their definitions, making a bloated challenge that's only really fun in one or two languages anyway.

The particular challenge you posted seems trivial to formalize in a language-agnostic way, by which I mean with mathematical notation. Actually, the math would be much simpler than that used in loads of problems on CGCC

And on top of it, I think that formalization would actually be much easier to read for most than the Lean code you posted. No?

Bubbler

1:47 AM

1. You need to define what a proof is in language-agnostic way. Can you? I tried but failed.

AviFS

You know way more about theorem-proving challenges on CGCC than I do, Bubbler. I'm just jumping into the deep end!

Bubbler

2. Even if we restrict to known theorem-proving languages, the necessary definitions to form the statement must be presented per language (and the writer should make sure that the definitions actually work as intended), which is only an extra hassle to the challenge writer

lyxal

@AviFS haha it took me 3:32

@AviFS yeah that got me too

AviFS

I know you guys have been trying to make good theorem-proving challenges for way longer than I've been here. I don't mean to question you guys!

@lyxal I finally got it for the "glasses" one, haha

Bubbler

You just questioned our decisions though

AviFS

1:52 AM

Right, I know! But like, an innocent question. I just wanted to clarify that I know you guys have put a lot of energy into this and I'm just jumping in, because it seemed like the answer was involved and I didn't mean for it to be taken personally like at all. And I couldn't tell if you were! Communication can be really hard over text!

Redwolf Programs

4:41

AviFS

The fact that you used bold, added a number one at the beginning, and then said "Can you? I tried but failed" made me wonder if the question was taken as imposing!

lyxal

@RedwolfPrograms get good

AviFS

So have we never had successful language-agnostic theorem proving challenges before, then?

Bubbler

We never had one, except for proof-golf which were about proving something without using any language

AviFS

1:57 AM

@Bubbler Those I've seen! Well I can definitely do a bit more digging on the meta then, and maybe wait until I have something put together to propose before poking at the challenge

Note to self: We should spotlight this answer for one of the yearly things.

It's a very hard question and there are only two answers. The older one has 28 upvotes, but the newer and winning one, by far, has only 3 (now 4).

Bubbler

Nah, it wasn't written in 2021, so it doesn't qualify for yearly best of

You can propose as an underappreciated answer here though

@AviFS If you're thinking about listing Lean's axioms and asking for a proof-golf, please don't. The logic of CIC (calculus of inductive constructions, the basis of Lean and Coq) doesn't fit in one page and it takes forever to derive anything interesting from the ground up

Sandbox Posts

3:38 AM

0

A: Sandbox for Proposed Challenges

Lean golf: List Game (rev_rev) The title is an homage of the Natural Number Game, which is a nice interactive tutorial into proving certain properties of natural numbers in Lean. Given that the previous two were slightly too involved (either mathematically or technically) for newcomers to Lean (i...

AviFS

3:54 AM

@Bubbler Yeah, thanks that's what I meant!

@Bubbler Definitely wasn't even thinking of considering to do that! Thanks though, haha. I'm thinking about asking for a proof without listing any axioms at all, and then seeing where different mathematical systems and proof techniques/langs take it. I don't know if it'll work but those are the lines I was thinking along.

Bubbler

Proof without axioms is way too broad. Every mathematical theory needs to start somewhere (natural numbers start with Peano's axioms, for example)

hyper-neutrino

is it even possible to prove anything without axioms?

doesn't incompleteness prevent that or am i remembering things wrong

Bubbler

And if you can assume arbitrary axioms, how would you prevent people from taking the task itself as an axiom?

@hyper-neutrino I mean, proof without (fixed set of) axioms

hyper-neutrino

ah

caird coinheringaahing

Only on SO

Bubbler

4:04 AM

Gold = Bronze + Silver (almost). That's... crazy :P

caird coinheringaahing

Honestly, I doubt that anyone could legitimately complete 211000 reviews competently

Bubbler

Agreed

Redwolf Programs

It's SO, if you're providing useful feedback instead of downvoting and moving on, you're doing it wrong :p

Throw in some canned comments if you're feeling extra

caird coinheringaahing

It feels bad to single out this user, but I genuinely believe that the top reviewers on SO, at least sometimes, use robo-review scripts

Redwolf Programs

Idk, 211000 is probably less than it seems on a site with as many review tasks to do as SO

If you take 20s per review task, that's just 48 days straight of reviewing

Which is a lot, but divided over several years I could see that being possible

And I'd think after 200k, any patterns caused by robo-reviewing would've been spotted

caird coinheringaahing

4:10 AM

Wait

It's been "today" for 4 hours so far, and each queue has a limit of 40 reviews. So how does this user have 80 already?

Redwolf Programs

It appears the limit is 80 for them

pVC aecidiospore adduced

@RedwolfPrograms do you have Divisions in biology / physics / geography/ computer??

Redwolf Programs

Bubbler

That link redirected to a regular review task for me, and it shows "Your daily reviews 0 /80" for me

hyper-neutrino

yeah when i go to the queue, at least FQ shows the limit is 80

caird coinheringaahing

4:12 AM

I got the link wrong, then corrected it btw

Redwolf Programs

@pVCaecidiosporeadduced ~~No, we only do division in math class~~

hyper-neutrino

yeah all are 40 except LQA, LA, and FA are 20, and FQ is 80

caird coinheringaahing

Also, this [faq] on MSE needs updating

@hyper-neutrino Hmm, forgive my suspicion for a user having already hit the limit, when the next highest is 39

Bubbler

So many queues :P

Redwolf Programs

@RedwolfPrograms Where I am, all of those are separate classes (Biology / Biology AP, Physics / Physics AP, World Geography / Human Geography AP, Computer Science A AP)

hyper-neutrino

4:14 AM

@cairdcoinheringaahing yeah, it looks very weird on first glance to me too :P (for me, the next is 40, which is exactly the limit i thought they had lol)

caird coinheringaahing

I cannot see anything here mentioning raising the limit to 80

hyper-neutrino

might just be SO-specific

all of ours seem to be 20 (although except during the height of our activity i don't think we've ever even generated 20 tasks in one queue in a day)

caird coinheringaahing

@Catija Can you confirm whether the limit has been raised to 80/day and if so, in which queues? I literally cannot find anything relevant searching for "[review] 80" on MSE

Bubbler

I found a reference here on MSO

which was posted less than a day ago

Redwolf Programs

I love how Spanish's "miles de kilómetros" looks like it'd mean "miles of kilometers" :p

Bubbler

4:20 AM

> The daily review quota has recently been increased from 40 to 80 for just the First Questions Review Queue, and only when the queue has more than 1000 items in it.

caird coinheringaahing

@Bubbler I shoulda waited a few seconds as not to ping Catija :/

Bubbler

It's somewhat like SO runs a different software from the rest of the network

pVC aecidiospore adduced

@RedwolfPrograms whats that AP?

Redwolf Programs

Advanced Placement

Basically for us, we're required to take at least four math, science, and history classes (plus other stuff, of course) in order to graduate. So things like biology and physics are year-long science classes specific to that subject. Same with history (they group geography in with that). Computer science is a bit different, since it's not required.

lyxal

@RedwolfPrograms how long do you have left until you graduate from school?

Redwolf Programs

4:29 AM

I'm in 10th grade now, so just over two and a half years.

Unrelated String

i have never been able to think of you as that much younger even though i feel you've mentioned it before

5

Redwolf Programs

It's okay, I'm going to catch up to y'all soon then we can all be the same age together

pVC aecidiospore adduced

> Movement of the earth on its axis is called as Resolution

lyxal

duh

why else do you think they're called New Years Resolutions /s

Razetime

@RedwolfPrograms just go to that one beach which makes you old

AviFS

4:41 AM

@Bubbler Programming without primitives is way too broad :p

@Bubbler And if you can assume arbitrary primitives, how would you prevent people from using/writing an esolang where the task itself is a primitive

Redwolf Programs

Oh hey, tomorrow's friday already

See y'all then o/

AviFS

@pVCaecidiosporeadduced Supposedly it means it's a college level class in the States. In my experience, college classes are way easier ; )

Razetime

@RedwolfPrograms cya

pVC aecidiospore adduced

Aaroneous needs to wait 3 hours before i give him 50 rep

why the 3 hours?

hyper-neutrino

bounties can't be started within i think it's 48h if that's what you mean

Bubbler

4:47 AM

@AviFS We don't prevent it, we just say "please don't, it's boring"

AviFS

It was a rhetorical question, though!

Bubbler

Well yeah, I got that, but still

AviFS

I don't know that it'll work. Not by a long shot. But one can hope that some of the same norms & upvoting logic will carry over

caird coinheringaahing

5:15 AM

@UnrelatedString Ikr, the fact that Redwolf is 3 or 4 years younger than me is O.o

lyxal

wait 3 or 4?

dang

I thought Redwolf was only 2 years younger

caird coinheringaahing

Also, in case anyone is wondering why I'm awake at 6am, its because, until literally 10 seconds ago, the parking garage across the road from me has had its fire alarm running non-stop since 10pm

@lyxal IIRC Redwolf is either 15 or 16

lyxal

@cairdcoinheringaahing oof. You don't have earplugs/noise-cancelling headphones/etc?

caird coinheringaahing

I have noise cancelling headphones, but I can't wear them when I sleep

lyxal

Wait fire alarm? Did no one else think to do something about it?

caird coinheringaahing

5:19 AM

@cairdcoinheringaahing Oh, I was wrong. They haven't stopped it, they're just running it at on/off intervals of around 30 seconds

@lyxal Nope

pVC aecidiospore adduced

[>+<-]

caird coinheringaahing

I live next to a police station as well, nothing from them either

pVC aecidiospore adduced

if bf had variables that store code

caird coinheringaahing

Isn't that just a function?

lyxal

@cairdcoinheringaahing but surely you're not the only one who had their sleep disturbed by the fire alarm.

pVC aecidiospore adduced

5:21 AM

@cairdcoinheringaahing y..yes

caird coinheringaahing

@lyxal I'd imagine not

pVC aecidiospore adduced

6:52 AM

time for geography exam

@Adám maybe add italics to APL386?

Adám

@pVCaecidiosporeadduced that'd be a huge job!

pVC aecidiospore adduced

@Adám how many glyphs does it have?

Adám

@pVCaecidiosporeadduced 892, but many are symbols that wouldn't be affected.

pVC aecidiospore adduced

7:08 AM

@Adám like: ⍺⍵⍒Σ?

and : +-×÷⍝⍀/\⍎⍕;'?

Adám

Yeah.

pVC aecidiospore adduced

7:19 AM

my headphone is annoying

yes it is very annoying

lyxal

that's an odd name for headphones

I just call them headphones

Because I don't go around saying "I listen to music with my very annoyings"

I say "I listen to music with my headphones"

/s

pVC aecidiospore adduced

lol

Bubbler

insert another joking joke here

pVC aecidiospore adduced

JoKing vs joking

windows doesn't recognise a difference

JoKing = joking

windows yes

oh ok

technically all BASIC programs scream

Unrelated String

thanks for linking natural number game
i may have just burned like two hours on just getting to the power level but this is fun

pVC aecidiospore adduced

8:13 AM

how come i write 3 pages but my friend writes 7 pages

hyper-neutrino

8:36 AM

if i have my induction set up as i : n * (a + b) = n * a + n * b, why can't i use rw i, on succ n * (a + b) = succ n * a + succ n * b? (doing the nat num game rn)

is it cuz succ n doesn't "count" as a member of the naturals?

Bubbler

i's left side is the very specific pattern n * (a + b) for already fixed values of n, a, b, so it cannot match anywhere in succ n * (a + b) which is (succ n) * (a + b)

hyper-neutrino

oh, i see... well then i'm stuck cuz i don't have a succ_mul or any commutativity yet and i managed to make a loop by breaking succ down into addition lol

New Posts

0

Q: Lean golf: Balanced Bracket Sequence

A bracket sequence is a string that consists of the characters ( and ). There are two definitions of a balanced bracket sequence. Definition 1 The empty string is balanced. If a string x is balanced, "(" + x + ")" is also balanced. If x and y are two balanced strings, x + y is also balanced. De...

code-golf balanced-string proof-golf lean

Bubbler

I guess I'll need to re-complete the nat game on every device I have, to figure out where the others are :P

hyper-neutrino

i ended up rewriting it from the top and picking another thing to do induction on lmao

Bubbler

8:50 AM

Please come to the Lean chatroom if you have any questions about Lean challenges or the Natural Number game.

6

Yeah, knowing how to pick which variable to induction is one of big skills in theorem proving

pxeger

@RedwolfPrograms just go to space and travel at the speed of light for a few years (or would that make you even younger? I'm no good at relativity)

Bubbler

Time to kill the nat game at the office PC

Adám

@pxeger Yes, faster travelling makes time progress slower, so one ends up lagging behind the rest of the world.

New Posts

9:11 AM

0

Q: i made this thing on a bytebeat composer named dollchan. do you like it? (11025Hz)

(t%200|t%201>>2)|(t>>4^1000|t%202)

code-golf math code-challenge music

hyper-neutrino

what?

pxeger

seems to be a way of generating music using what are essentially hash formulae

but it's just more butter

Bubbler

9:33 AM

... and I just realized that the nat game mysteriously fails to load here

frick

7

pVC aecidiospore adduced

9:49 AM

@NewPosts how much rep do i need to veiw deleted posts

Bubbler

10k

New Posts

10:24 AM

0

Q: Revert Flow Free puzzle

Inspired by Is this Flow Free puzzle trivial? by @Bubbler. Lengthy chunks of this challenge are borrowed from there. This may be one step of a solution for the linked challenge, depending on chosen strategy. Background Flow Free is a series of puzzle games whose objective is to connect all the sa...

code-golf array-manipulation grid

user

11:24 AM

@pxeger No, redwolf should go to the moon and accelerate the earth away from him

Adám

@pVCaecidiosporeadduced Do you know about this list?

Sandbox Posts

12:38 PM

0

A: Sandbox for Proposed Challenges

Give me the border code-golfarray-manipulation Inspired by Is this Flow Free puzzle trivial? by @Bubbler. Lengthy chunks of this challenge are borrowed from there. This may be one step of a solution for the linked challenge, depending on chosen strategy. Challenge Given an array of digits 1-9 and...

caird coinheringaahing

12:55 PM

Just a PSA: please don't vote to delete questions that are closed as "Needs details or clarity", (example), especially if they have answers, as, however unlikely, the OP may come back and attempt to fix the challenge. If these posts really should be deleted, then the automated Roombas will clean them up. Save your VTDs for things that should be removing as quickly as possible (e.g. butter, spam, etc.)

It also doesn't help that deleting these posts undoes the reputation earned by the answers, if done within 60 days of posting :/

lyxal

@NewPosts y'know, I was always wondering why it's called "Flow Free" in the title of both questions, because I was like "why tf you referencing the free version? Isn't the paid version literally just the same puzzle" but then I saw that "free" is quite literally part of the name of the app and that there is no flow paid

This is so sad alexa play despacito

caird coinheringaahing

@lyxal why is it sad that there isn't a paid version?

lyxal

Because I was going to purchase it from the play store to make a joke along the lines of "y'all playing the free version while I'm being a gamer playing the paid version"

And that would have potentially resulted in 4 or 6 stars on the starboard because it would have been a haha funny joke

Now I've got no haha funny joke on the starboard and it's time for bed

Hence why I need alexa to play despacito

caird coinheringaahing

I have to say, I've never considered paying in order to get something on the starboard :P

lyxal

well it's not like it's my money anyway

I would have just used the free play store credits I get from doing google surveys lol

I'm desperate for validation via meaningless stars, but not that desperate to use my own money

caird coinheringaahing

1:02 PM

@lyxal If you're stealing money in order to finance TNB jokes, we may have to have an intervention for you :P

lyxal

@cairdcoinheringaahing why you gotta be a spoilsport like that? Everyone knows that you don't get stars without some sort of illegal funding /s

caird coinheringaahing

Yeah, but stealing is the worst form of illegal funding. Do what the rest of us do and enter into a pact with the God of Code Golf

lyxal

Heck no

Stealing is original

And I'm all about original

caird coinheringaahing

Isn't stealing, almost by definition, not original? :P

Bubbler

If anyone's wondering, I enjoyed all three games in the Flow Free series (vanilla, Hexes, Warps), grinding for all achievements (which include three "play 365 daily puzzles")

(and if you want Flow VIP, just buy all packs + remove ads. I did for all 3, and they're worth it)

Transcript for