Conditional acceptance tactic and Bayesian scoring

Stream: new members

[Michael Bucko]

I am reading Metaprogramming in Lean 4, and was wondering if it's possible to write a tactic that could accept my Nat.radical (even though it's not defined), and simply allow it (perhaps marked as conditionally accepted), given what it knows about Ideal.radical?

[Eric Wieser]

What do you mean by "accept"?

[Yaël Dillies]

I'm afraid you need to be able to read our DMs to understand the question:
Yaël Dillies said:

I would suggest defining Nat.radical separately to Ideal.radical and then show Ideal.radical (Ideal.span {n}) = Ideal.span {Nat.radical n}

[Michael Bucko]

Accept (conditionally) = subgoal conditionally proven (perhaps given some evidence).

[Michael Bucko]

Some background:

• Regular (or even an LLM-driven) autocomplete is suboptimal,
• Function names are quite informative, but it takes quite a bit of time to find them
• Sorry is great, but feels very binary

The idea would be to have an ELO-like scoring system for proof writing. One could approach this from the Bayesian angle. That could enable more automated knowledge discovery.

The way to start all this would be to enable probabilistic completion / conditional acceptance.

[Michael Bucko]

Essentially, the tactic would probabilistically accept subgoals and provide the conditional probabilistic score of the proof.

In the case @Yaël Dillies mentioned, I found Ideal.radical, but needed a different one, and then @Yaël Dillies made some suggestions; eventually, I ended up rewriting stuff, which is most likely suboptimal (, i.e. even if my new proof is 100% correct, I'd still prefer to see a probabilistic suggestion / and have it reflected in the tactic state).

What do you think?