Non-co-semi-decidability of LEF groups

Let $\mathcal{G}_{WP}$ be the space of marked groups with solvable word problem, and let $\Lambda_{WP}$ denote its word-problem representation. A group is LEF when it belongs to the closure of the set of marked finite groups. A property is $\Lambda_{WP}$-co-semi-decidable when its complement is semidecidable relative to $\Lambda_{WP}$.

LEF non-co-semi-decidability conjecture. The set of LEF groups is not $\Lambda_{WP}$-co-semi-decidable.

The conjecture is motivated by the undecidability of the universal theory of finite groups and is proposed as a natural failure of the correspondence between Borel and arithmetical hierarchies. It remains open.