I was working through the intuitionistic soundness theorem and came up with a proof, but had a critical insight when I trying to understand the mechanics of completeness. It looks like the soundness theorem works equally well for terms that denote false – for which the only satisfying value will be ⊥. That's fine and even expected for soundness – we can prove false things by putting falsehoods into Γ, and indeed any proof of a tautology of the form ~A will do exactly this.

But for valid_of_provable it seems like we need something stronger – that ∅ ⊨ A is non-bottom for any valuation, in some Heyting algebra H (perhaps every non-trivial Heyting algebra H). We'll need something similar for completeness as well.

This is 90% a me problem given my unfamiliarity with lean, but on the 10% chance it is a mistake in the repo:

For some reason I was unable to get the repo itself working, but the examples seemed standalone so I imagine they would work if they were pasted into a working lean project

Following the example in https://github.com/PatrickMassot/GlimpseOfLean/blob/master/GlimpseOfLean/Exercises/01Rewriting.lean#L155

When I write the code:

import Mathlib
import Lake
open Filter 

example (a b c d : ℝ) (h : c = d*a - b) (h' : b = a*d) : c = 0 := by {
  rw [h'] at h
  ring at h
  -- Our assumption `h` is now exactly what we have to prove
  exact h
}

I got an error:

unexpected token 'at'; expected '}'