Understanding what Aristotle is formalizing

Stream: Machine Learning for Theorem Proving

[J. J. Issai (project started by GRP)]

I had someone send me a formalization generated by Aristotle for a couple of statements. I don't (yet) have access to the original query, so the problem might be a misstatement in the query. However, the output from Aristotle seems not to track.
I want to formalize a couple bounds on the pcf (prime counting function), which I write as pi(x) being the set of primes <= x. (I am using this to decide whether to go with pi(x) or pi(n), where n will be natural instead of real.) One of the bounds is forall real x>0 , pi(x)<= ceil(x/2). Here is the output of Aristotle:

theorem pcf1 {x : ℝ} (hx : 0 < x) : Nat.primeCounting' ⌊x⌋₊ ≤ ⌈x / 2⌉ := by
  -- We'll use that π(n) ≤ n/2 for all n ≥ 2.
  have h_pi_le_half : ∀ n : ℕ, 2 ≤ n → Nat.primeCounting' n ≤ n / 2 := by
    intro n hn; induction hn <;> simp_all +arith +decide [ Nat.primeCounting', Nat.succ_eq_add_one ] ;
    cases Nat.Prime.eq_two_or_odd ( Nat.prime_two ) <;> simp_all +arith +decide [ Nat.count_succ ];
    split_ifs <;> simp_all +arith +decide [ Nat.add_div ];
    · cases Nat.Prime.eq_two_or_odd ‹_› <;> simp_all +arith +decide [ Nat.count_eq_card_filter_range ];
    · exact le_add_of_nonneg_of_le ( by positivity ) ‹_›;
  by_cases h₂ : 2 ≤ ⌊x⌋₊;
  · -- Since $\lfloor x \rfloor \leq x$, we have $\lfloor x \rfloor / 2 \leq x / 2$. Taking the ceiling of both sides, we get $\lceil \lfloor x \rfloor / 2 \rceil \leq \lceil x / 2 \rceil$.
    have h_ceil : ⌈(⌊x⌋₊ : ℝ) / 2⌉ ≤ ⌈x / 2⌉ := by
      exact Int.ceil_mono <| by linarith [ Nat.floor_le hx.le ] ;
    refine le_trans ?_ h_ceil;
    exact Int.le_of_lt_add_one ( by rw [ ← @Int.cast_lt ℝ ] ; push_cast; linarith [ Nat.div_mul_le_self ⌊x⌋₊ 2, Int.le_ceil ( ( ⌊x⌋₊ : ℝ ) / 2 ), show ( Nat.primeCounting' ⌊x⌋₊ : ℝ ) ≤ ⌊x⌋₊ / 2 from by exact le_trans ( Nat.cast_le.mpr ( h_pi_le_half _ h₂ ) ) ( by rw [ le_div_iff₀ ] <;> norm_cast ; linarith [ Nat.div_mul_le_self ⌊x⌋₊ 2 ] ) ] );
  · interval_cases _ : ⌊x⌋₊ <;> norm_num [ Nat.primeCounting' ];
    · positivity;
    · positivity

Two things concern me:
One is that primecounting' is used, instead of primecounting. If I read this correctly, Aristotle is showing that (when floor(x)=n) pi(n-1) <= ceil(x/2) = ceil(n/2). Am I reading the theorem statement of Aristotle correctly?
The second is that I read the first comment as using that pi(n)<= n/2 for n>=2. This comment fails for n=3 upon a literal reading. So what is Aristotle actually using? (It seems to be pi(n-1)<= n/2, which I can believe but falls short of my goal. Is Aristotle using this?)
I have not fed (the file containing this) to Lean to verify that it compiles.

[Yury G. Kudryashov]

Is your question specifically about Aristotle or about reading Lean code in general? It's hard to say if Aristotle correctly autoformalized the input without the original query at hand. Indeed, the estimate uses Nat.primeCounting', so it may be worse than your goal by 1. About comments, while they're generated with the formal proof, they may be wrong, because they aren't formally verified. haves are the ultimate source of truth about the path Aristotle takes in the proof.
P.S.: Please use #backticks for code, including inline, and double dollars for $\LaTeX$.

[J. J. Issai (project started by GRP)]

In this case the question is about reading a specific piece of Lean code, which was generated by Aristotle. Without drilling deep into this example, I might blindly accept it if it compiled or reject it based on the troublesome comment. Contained in this is the assertion that Aristotle may have one view of $\pi(x)$, and I have another view of pi(x). If I can't reconcile these views, I can't trust Aristotle. So the question is also about Aristotle's view of the problem.

[Yury G. Kudryashov]

You don't have to trust Aristotle. You should learn enough about Lean/Mathlib to read statements, then verify that Lean successfully compiles outputs.

[Yury G. Kudryashov]

Note that we're still on v4.24, not on the lastest version. We'll post here on Zulip when we upgrade.

[Mario Carneiro]

docs#Nat.primeCounting'