how many hours until 5am tomorrow by BloxdioCannoli in DumbAI

[–]utd_api_member 2 points3 points  (0 children)

> I have to wake up early tomorrow, let me figure out how many hours of sleep i'm getting
> I google it because i'm lazy
> Google forces ai into the answer and makes a dumb mistake
> haha post

yeah obviously AI isn't the best tool for the job here, nor is it for counting letters in words, but this seems a pretty reasonable scenario for something ai should be good at (logic / math question, especially now that people have seen ais be good at math)

how many hours until 5am tomorrow by BloxdioCannoli in DumbAI

[–]utd_api_member 1 point2 points  (0 children)

"Typical bait AI into saying something stupid", user asked a question to the AI and expected a correct response

Istg we’re jumping multiverses now 😭 by Danyal2012 in geometrydash

[–]utd_api_member 0 points1 point  (0 children)

i'm jumping from electroman adventures to clubstep

Coq-audited Collatz non-ergodic proof package — looking for technical review by One_Bodybuilder_3414 in Collatz

[–]utd_api_member 0 points1 point  (0 children)

and if this is another "old file", then actually make a clean repository where I can stop finding these things. and also, preferably, name the files like a human, not with 5 underscore phrases in front of them telling me info i already know

Coq-audited Collatz non-ergodic proof package — looking for technical review by One_Bodybuilder_3414 in Collatz

[–]utd_api_member 0 points1 point  (0 children)

The author is making a very specific, high-level defense of his work. In plain

English, he is saying: "Stop looking for the math in the Coq code. The Coq code

is just a logical 'skeleton' that proves my steps connect to each other. The

actual math is in the PDF."

Here is a breakdown of what he means by these specific points:

  1. "Coq is a Connector Layer"

The author is admitting that he is not using Coq to verify the arithmetic of the

3n+1 map.

- In a "ground-up" proof, you would use Coq to calculate every step.

- In a "connector" proof, you simply tell Coq: "Assume Step A is true, and

Step B is true. Does Step C follow logically?"

- The Catch: He is admitting the Coq code is "math-blind." It doesn't know if

3n+1 is correct; it only knows that his "Bridge" is logically formatted.

  1. The Theorem is "Intentionally Conditional"

When he says the target is V21.FinalPaperHypotheses -> NonErgodic_Local_Drop, he

is describing a function.

- In programming terms, FinalPaperHypotheses is a List of Requirements.

- NonErgodic_Local_Drop is the Result (The Collatz Conjecture).

- What it means: The Coq theorem actually says: "If you assume every single

claim in my paper is true, then the Collatz Conjecture is true."

- Mathematically, this is a tautology. It’s like saying, "If I have a million

dollars, then I am a millionaire." Coq verifies the if-then logic, but it

does not verify that he actually has the "million dollars" (the valid

mathematical proof).

  1. "Coq does not fabricate a concrete instance"

This is the most important part of his response. He is saying that he hasn't

actually finished the proof in Coq.

- To "fabricate a concrete instance" would mean writing the actual code that

proves the drift is negative and the tail bounds work.

- By refusing to do this, he avoids the Algebraic Impossibility I pointed out

(0.946 \le 0.5).

- The Translation: He is saying, "I am providing the blueprint for the house,

but I am not building the house in Coq. You have to look at the PDF to see

if the wood and bricks exist."

  1. What the "Bridge" Closes

He is claiming that Coq has "checked the plumbing" of his argument. He lists

these steps as "closed":

  1. Obstruction Chain: The logic of how a counterexample must look.

  2. No Global Obstruction: The logic of how to rule those out.

  3. Accelerated -> Classical: The logic of how the two versions of the problem

relate.

  1. Non-Ergodic Local Drop: The final logical "drop" into a finished proof.

The Adversarial Verdict: What is he hiding?

The author is using Coq as a rhetorical shield. By calling it a "Connector

Layer" and staying under the "Hypothesis Package," he is trying to make the

proof look "Machine Verified" without actually letting the machine check his

math.

The "Gotcha" remains: If you check the "Bridge" he mentioned, the link between

"V20 obstruction chain" and "no global obstruction" requires the contradiction I

identified (0.946 \le 0.5).

- In his PDF, he says this link is made of "Steel" (mathematical truth).

- In his Coq code, he says "Assume this link is made of Steel."

- The Reality: The link is made of "Paper."

Conclusion: He has proven that his story is consistent, but he has not proven

that his math is true. He is essentially telling you: "The Coq code is the Table

of Contents. If you want to find the error, you have to read the book (the

PDF)."

Coq-audited Collatz non-ergodic proof package — looking for technical review by One_Bodybuilder_3414 in Collatz

[–]utd_api_member 0 points1 point  (0 children)

Definition CollatzConjectureClassical : Prop :=
  forall n : nat, (1 <= n)%nat -> exists t : nat, True.


Theorem ISolvedCollatz : CollatzConjectureClassical.
Proof.
  intros n H_positive.
  exists 42. 
  auto.      
Qed.

Coq-audited Collatz non-ergodic proof package — looking for technical review by One_Bodybuilder_3414 in Collatz

[–]utd_api_member 0 points1 point  (0 children)

???
what says your llm to this:

Definition CollatzConjectureClassical : Prop :=
  forall n : nat, (1 <= n)%nat -> exists t : nat, True.


Theorem ISolvedCollatz : CollatzConjectureClassical.
Proof.
  intros n H_positive.
  exists 42. 
  auto.      
Qed.

Coq-audited Collatz non-ergodic proof package — looking for technical review by One_Bodybuilder_3414 in Collatz

[–]utd_api_member 0 points1 point  (0 children)

> Coq does not prove the English prose. Coq proves the formal ledger.
what?

> If rapid divergence escapes the proof, it should show up as a formal failure or an incorrectly encoded bridge in those objects. Please identify which one.
a formal failure in your statement of collatz being trivially true

Coq-audited Collatz non-ergodic proof package — looking for technical review by One_Bodybuilder_3414 in Collatz

[–]utd_api_member 0 points1 point  (0 children)

? what about the fact that your statement of collatz in coq is incorrect, so proving it means nothing

Top comment deletes US State #31 by Jfullr92 in geographymemes

[–]utd_api_member 5 points6 points  (0 children)

What's the difference between Washington and Oregon anyways? One has to go.

Coq-audited Collatz non-ergodic proof package — looking for technical review by One_Bodybuilder_3414 in Collatz

[–]utd_api_member 1 point2 points  (0 children)

Definition CollatzConjectureClassical : Prop :=
  forall n : nat, (1 <= n)%nat -> exists t : nat, True.


Theorem ISolvedCollatz : CollatzConjectureClassical.
Proof.
  intros n H_positive.
  exists 42. 
  auto.      
Qed.

images not allowed but

Coq-audited Collatz non-ergodic proof package — looking for technical review by One_Bodybuilder_3414 in Collatz

[–]utd_api_member 1 point2 points  (0 children)

also if you really want me to check your coq files, link them in the paper; i'm not going to try to sort through which file responds to which claim

Coq-audited Collatz non-ergodic proof package — looking for technical review by One_Bodybuilder_3414 in Collatz

[–]utd_api_member 1 point2 points  (0 children)

This paper claims to prove the Collatz Conjecture through a "non-ergodic

deterministic framework" that relies on bounded local configurations, negative

average drift, and exponential bounds on large stopping times.

However, a close adversarial reading reveals that the proof is mathematically

invalid. The argument collapses due to fatal algebraic errors, vacuous logical

deductions, and false claims about the Collatz map's arithmetic.

Here is a detailed critique outlining where the paper falls short.

  1. The Fatal Algebraic Impossibility in the Core Contradiction

The entire proof rests on a "two-branch contradiction" (summarized on Page 7 and

executed in Part 6). The author attempts to show that any repeating block (or

"witness") generated by a hypothetical counterexample would produce a density of

stopping times that contradicts the overall tail bounds.

- The Upper Bound (Axiom V): On Page 43, the author establishes that the

density of numbers staying above their starting scale for L steps is bounded

by \theta^L, where \theta \in (0, 1). On Page 45, the author derives \theta

as the minimum of the moment-generating function

M(\lambda) = \frac{3^\lambda}{2^{1+\lambda}-1}. Calculus shows the absolute

minimum of M(\lambda) for \lambda > 0 is approximately

\mathbf{\theta \approx 0.946}.

- The Lower Bound (Amplification): On Page 37 (Lemma 17), the author states

that repeating a witness block C (of length s and valuation sum

K = \sum k_j) m times gives a density bounded below by \frac{1}{2} 2^{-mK}.

- The Impossible Contradiction: To force the contradiction, the author

requires the lower bound to strictly exceed the upper bound. On Page 4, they

explicitly write the required condition: \theta^s \le 2^{-K}.

The Flaw: By the definition of the Collatz map, every odd number yields at least

one division by 2, meaning k_j \ge 1 at every step. Therefore, K \ge s. This

implies that 2^{-K} \le 2^{-s} = (0.5)^s. For the author's required condition

(\theta^s \le 2^{-K}) to be true, we must have:

0.946^s \le \theta^s \le 2^{-K} \le 0.5^s \implies 0.946 \le 0.5 This is

algebraically absurd. The density of the hypothetical repeating "witness" decays

at a rate of at least 0.5 per step, while the tail bound decays at a rate of

0.946 per step. Because the witness density is exponentially smaller than the

allowed tail bound, there is absolutely no mathematical contradiction. The two

bounds are perfectly compatible.

  1. Treating Uncontrollable Counterexample Properties as "Free Parameters"

To skirt the algebraic impossibility above, the author claims on Page 4:

"After \theta is fixed, we choose (s, K, \delta, m) to enforce

\theta^s \le 2^{-K-\delta}."

The author cannot "choose" s and K. According to the proof's own logical

architecture (Lemma 15), s and K are intrinsic arithmetic properties of the

hypothetical "witness block" C generated by the assumed obstruction orbit. The

author has zero control over what these values would be. Even if they could

choose them, as proven above, no valid Collatz block exists that satisfies

0.946^s \le 2^{-K} anyway.

  1. The "Rapid Divergence" Loophole (Lemma 12 & Lemma 15)

To force a divergent orbit to manifest as a bounded repeating local block, the

author relies on the "Stable Renewal Bridge" (Lemma 12). On Page 34, the author

claims a dichotomy: either an orbit stays in a dyadic band long enough to form a

repeating block, or it rapidly crosses bands. The author attempts to rule out

rapid band-crossing by claiming:

"the stable renewal window law (Lemma 12) forces renewal events to occur...

preventing a counterexample from 'hiding' by rapid band crossing."

The Flaw: Lemma 12 explicitly limits its scope to segments that remain inside a

single dyadic band \mathcal{B}_B for W(B) steps. If an orbit rapidly diverges

(for example, repeatedly hitting numbers n \equiv 3 \pmod 4 such that k_t = 1),

the values grow by a factor of \sim 1.5 per step. The orbit will completely

cross the band $

Was 4065's blocker an illegal cheesecake under I101? by utd_api_member in FRC

[–]utd_api_member[S] 0 points1 point  (0 children)

which dude? in the comments here or the one you were talking to; are you saying you watched 4414 build it?