zombie proof processes

[Manuel Eberl]

Just FYI, we have a lot of material on the harmonic numbers in the 
distribution already. Including of course the fact that they're 
unbounded. E.g. in HOL-Analysis.Summation_Tests:

> lemma not_summable_harmonic: "¬summable (λn. inverse (of_nat n) :: 'a 
> :: real_normed_field)"
Or, expressed in a different way:

> definition✐‹tag important› harm :: "nat ⇒ 'a :: real_normed_field" where
>   "harm n = (∑k=1..n. inverse (of_nat k))"
> theorem not_convergent_harm: "¬convergent (harm :: nat ⇒ 'a :: 
> real_normed_field)"
Or a more precise lower bound:

> lemma harm_ge_ln: "harm n ≥ ln (real n + 1)"
And a lot more.


Cheers,

Manuel




On 11/28/25 20:57, Peter Lammich wrote:
> Another one. veriT. Somewhere in my proof exploration of the below.
>
> I'll try to re-sledgehammer all goals in there, maybe it provokes a 
> rogue veriT again...
>
> -- 
>
>   Peter
>
>
> imports Complex_Main
> begin
>
>
> lemma upt_fuse: "⟦l≤m; m<h ⟧ ⟹ [l..<m] @ [m..<h] = [l..<h]"
>   by (metis less_imp_add_positive upt_add_eq_append)
>
>
> corollary harmonic_series_unbounded_aux: "n ≤ (∑i←[1..<2^(2*n)+1]. 1/i)"
> proof -
>
>   have A: "(real n+1)/2 ≤ (∑i←[1..<2^n+1]. 1/i)" for n
>   proof (induction n)
>     case 0
>     then show ?case by simp
>   next
>     case (Suc n)
>
>     (* It feels like we're working against the simplifier for [_ ..< 
> Suc _], so we disable that rule *)
>     find_theorems "[_..<Suc _]"
>     note [simp del] = upt_Suc
>
>     have SPLIT: "[1..< 2^Suc n + 1] = [1..< 2^n + 1]@[2^n + 1 ..< 
> 2^Suc n + 1]" (is "_ = ?l1@?l2")
>       by (simp add: upt_fuse)
>
>     from Suc.IH have "(real n+1)/2 ≤ (∑i←?l1. 1/i)" .
>     moreover have "1/2 ≤ (∑i←?l2. 1/i)" proof -
>       have 1: "(1/2 :: real) ≤ (∑i←?l2. 1/2^Suc n)" by (simp add: 
> sum_list_triv)
>       have 2: "(∑i←?l2. 1/2^Suc n) ≤ (∑i←?l2. 1/i)"
>         apply (rule sum_list_mono)
>         apply (clarsimp simp: less_Suc_eq_le)
>         apply (drule of_nat_mono[where j="2*2^_"])
>         by (auto simp: field_simps)
>       from order_trans[OF 1 2] show ?thesis .
>     qed
>     ultimately show ?case
>       apply (subst SPLIT)
>       by simp
>   qed
>
>   show ?thesis
>     apply (rule order_trans[OF _ A])
>     by auto
> qed
>
>
>
> lemma harmonic_series_unbounded: "∃n. c ≤ (∑i←[1..<n]. 1/i)"
> proof -
>   have "c ≤ (nat ¦⌈c⌉¦)" by linarith
>   also note harmonic_series_unbounded_aux
>   finally show ?thesis by blast
> qed
>
>
> On 28/11/2025 17:56, Makarius wrote:
>> On 28/11/2025 17:40, Peter Lammich wrote:
>>>
>>> On 28/11/2025 17:16, Lawrence Paulson wrote:
>>>> As it is intermittent, I was wondering whether certain 
>>>> characteristics of the goal might cause this.
>>>>
>>>> Is your example reproducible?
>>>
>>> Unfortunately not. I only realized that this process was running 7 
>>> minutes after it was started ... no idea what I was sledgehammering 
>>> at this point :(
>>>
>>> I typically realize that only when I keep hearing my CPU fan, and my 
>>> CPU temperature keeps being high, although no proof or sledgehammer 
>>> is running.
>>
>> Peter,
>>
>> that is new information: the problem happens on Linux, and for 
>> Isabelle2025 already. So it is not specific to macOS 26, nor to any 
>> changes towards Isabelle2025-1.
>>
>> I am still interested to learn about the reasons, but it is now more 
>> likely to get ticked-off as "non-regression" towards Isabelle2025.
>>
>>
>>     Makarius
>>