equation explorer I'm not feeling lucky

Stream: Equational

[Kevin Buzzard]

I was showing equational theories to a friend and noticed that the "I'm feeling lucky" button on https://teorth.github.io/equational_theories/implications/ didn't seem to do anything. Is this a known issue? Can anyone else reproduce? I thought there were two questions left?

[Shreyas Srinivas]

I think there is only one implication left from the original batch. Could be a result of that.

[Shreyas Srinivas]

Actually I can narrow it down a bit further. The equation explorer is likely getting slightly incorrect data at this function:

function findRandom8(implications) {
  // Find all coordinates with value 8
  const eights = [];

  for (let i = 0; i < implications.length; i++) {
    for (let j = 0; j < implications[i].length; j++) {
      if (implications[i][j] === "unknown") {
        eights.push([i, j]);
      }
    }
  }

  // If no 8s found, return null
  if (eights.length === 0) {
    return null;
  }

  // Pick a random coordinate from the found 8s
  const randomIndex = Math.floor(Math.random() * eights.length);
  return eights[randomIndex];
}

If I had to guess, it's an off by one error that is triggered because there is only one implication left

[Douglas McNeil]

Hmm, when I inspect it locally it looks like the implications array has the numerical values, not the string values, so === "unknown" is never going to work. If I override it to be === 8, I get more sensible eights entries, and then go to either 1729->817 or 1898->2644 for lean.

Maybe a side effect of the recent finite extensions to the explorer left implications in a different state than this function was expecting.

[Shreyas Srinivas]

CC: @Vlad Tsyrklevich

[Kevin Buzzard]

I also wasn't sure whether I expected it to jump to something whose status was unknown, or more generally something whose proof hasn't been formalised yet

[Vlad Tsyrklevich]

Is it worth keeping now that there's 1 unknown left? I can investigate fixing it later, but maybe it has also passed the point where it makes sense

[Kevin Buzzard]

I only wanted to use it to find out what the unknown question was because it's easier than reading 10000 messages in this channel

[Vlad Tsyrklevich]

Yeah it's maybe not clear that the way to find that is to 1) click "Hide fully-solved equations" and 2) unclick "Treat conjectures as unknown"

[Vlad Tsyrklevich]

Douglas had the correct root cause, this was broken by me in dc57f2db8d10c0dbc8c4fb4beea01d3589ceff3a when I sped up equation explorer loads by using integer values instead of strings in that array. Fixed in equational#842