João Marcoslogo_ttlM. Antonia Huertas, João Marcos, María Manzano, Sophie
Pinchinat,
François Schwarzentruber54th International Conference on Tools for Teaching
Logic11119TTL2015

# Fail Better: What formalized math can teach us about learning 111The author
acknowledges partial support by the Marie Curie project PIRSES-GA-2012-318986,
funded by EU-FP7, and by CNPq / Brazil.

João Marcos  UFRN, Brazil
<EMAIL_ADDRESS>
###### Abstract.

Real-life conjectures do not come with instructions saying whether they they
should be proven or, instead, refuted. Yet, as we now know, in either case the
final argument produced had better be not just convincing but actually
verifiable in as much detail as our need for eliminating risk might require.
For those who do not happen to have direct access to the realm of mathematical
truths, the modern field of formalized mathematics has quite a few lessons to
contribute, and one might pay heed to what it has to say, for instance, about:
the importance of employing proof strategies; the fine control of automation
in unraveling the structure of a certain proof object; reasoning forward from
the givens and backward from the goals, in developing proof scripts; knowing
when and how definitions and identities apply in a helpful way, and when they
do not apply; seeing proofs [and refutations] as dynamical objects, not
reflected by the static derivation trees that Proof Theory wants them to be.

I believe that the great challenge for teachers and learners resides currently
less on the availability of suitable generic tools than in combining them
wisely in view of their preferred education paradigms and introducing them in
a way that best fits their specific aims, possibly with the help of
intelligent online interactive tutoring systems. As a proof of concept, a
computerized proof assistant that makes use of several successful tools
already freely available on the market and that takes into account some of the
above findings about teaching and learning Logic is hereby introduced. To
fully account for our informed intuitions on the subject it would seem that a
little bit extra technology would still be inviting, but no major breakthrough
is really needed: We are talking about tools that are already within our reach
to develop, as the fruits of collaborative effort.

###### Key words and phrases:

mathematical thinking; computer-assisted instruction; proof assistants;
intelligent tutoring systems

###### 1991 Mathematics Subject Classification:

K.3.1 Computer Uses in Education; F.4.1 Mathematical Logic

##  1\. Ask yourself again: What is a Proof?

Non-obvious arguments have interesting inner structures: givens may be assumed
to be connected to goals by directed loop-free finite paths; each node of such
a structure would be annotated with some statement; the finite collection of
all edges concurring in a node $S_{m}$ would itself be annotated by a
justification according to which the statements $S_{1},S_{2},\ldots,S_{j_{m}}$
contained in their other endpoints would suffice for an appropriate
inferential link to be recognized; source nodes would be labelled in such a
way that some of them could be identified as temporary suppositions, and the
others as assumptions that would have been employed as starting points for the
corresponding argument. If one puts the corresponding directed acyclic graph
upside-down and unravels the paths to avoid a node to be visited more than
once, the sink nodes become roots of their own derivation trees. While
checking that such an argument has been constructed flawlessly according to a
number of inference rules set in advance essentially reduces to a rather
costless tree traversal task, the very task of constructing the goal-directed
argument, starting from the initial given hypotheses is however a potentially
costly problem that might require a lot of ingenuity to be solved. However,
real-life problems will often demand practitioners to construct precisely this
kind of interwoven structures concerning a given conjecture without a hint on
whether this conjecture is true or false — and often the arguments supporting
its truth are quite distinct from the arguments supporting its falsity. It
should be no wonder that students often have difficulty with mastering the
techniques for going about and develop their own arguments, and tutors often
have a hard time teaching students how to proceed.

Many tasks related to exploring conjectures by either proving or refuting them
may be fully automated, as, for instance, in cases in which complete decision
procedures are known to exist. Arguably, however, if students are to be more
than button-pushers for imported technological toys that play by themselves,
they have more to learn by implementing the decision procedures than by
actually using their tools to evaluate whatever conjecture needs to be
checked. At any rate, I believe students can learn many important skills even
when working with fully automatable theories, as long as they approach them in
a productive way, and I believe tutors have a lot to learn from the many
advancements that have been made in the fast-growing field of formalized
mathematics. The teaching principles subsequently discussed in the present
paper are intended to provide evidence for such beliefs.

##  2\. Lessons from formalized mathematics

Mathematics in the early 19th century was navigating a sea of uncalculated
logical gaps and gluts, with few safe harbors in which to dock. Its non-
systematic use of axioms and relatively careless use of definitions, found
amid a baroque prose that allowed for much ambiguity and imprecision to crop
in, resulted in a disgraceful state of affairs in which the mathematical
vessel appeared to be going adrift. Disaster seemed imminent, had it not been
by the masters of the trade not letting it sink. The forerunners of the now
venerable foundational schools strove to provide firm grounds for Mathematics,
and Logic had important roles to play in such quest. ‘Safe’ proof methods and
techniques were progressively identified, and stricter standards were imposed
for an argument to be considered acceptable. In the following century the very
notion of proof became a mathematical object in itself, and one whose
characterization and properties were to be deeply investigated.

The works of Gentzen and other wise forerunners of Proof Theory have not only
shaped the way we now think about proofs, but have heavily influenced the
ulterior design of mechanized proof-assistants. As a matter of fact, many
lessons in Logic seem to have been made clearer by implementations of such
proof-assistants than they had been for several earlier generations of ‘pure’
mathematical logicians, or early type theorists — as an example, one could
argue that the difference in the roles played by free and by bound variables
becomes more striking if you think of them as sorted into quantifier rules
that introduce parameters in contrast to those that introduce unknowns. My
contention in the present paper is that paying more attention into how novice
students interact with such tools for doing computer-assisted math might help
understanding other important lessons that would have remained unheard. I
propose to discuss some such largely understated lessons in what follows.

### Seeing proofs [and refutations] as dynamical objects.

You give your student an exam to be solved with pencil-and-paper. She has to
write a convincing argument that will lead to either proving or refuting a
given conjecture. Having been rightly taught that a mathematical proof is
about adequately justifying her conclusions and not about providing an
explanation of her thought processes (cf. [13]), the student hands back to you
a scratch of the logical structure of her argument, in the form of a
derivation tree. How did she arrive to it? You might never know. To the best
of your knowledge, she might have received the full argument ready from the
dancing hands of Shiva — or maybe from a fellow student.

This time you are the one scratching the skeleton of a proof in the
blackboard, in front of your student. Instead of cleanly proceeding from
hypotheses to conclusion, or maybe proceeding the other way around, you allow
yourself some false starts, backtrack from dead ends, get stuck here and
there, and fail in every possible way — having an eye at what can be learned
from such repeated failures. You exhibit the full plethora of feelings that
accompany the process of inventing/discovering a proof, including the mixture
of satisfaction and relief when you manage to fill all the blanks that
separate givens and goals. Your student will be happy to follow you
attentively, and then take a picture of the final result with her mobile
phone. When she arrives at home, though, she tries to retrace your steps, but
does not manage to reproduce the same derivation tree for the given conjecture
— or to produce any derivation tree at all.

In both situations, what is not being captured by the student is the dynamical
aspect of the proof object. The complete derivation tree that you find at your
student’s exam is wholly static, and the media in which it has been registered
does not allow you to replay its construction. The picture taken by the
student of the proof that resulted from your toil is only the last frame of a
movie. It might be the climax of the movie, but, more often than not, it does
not allow the interested spectator to recover details of the full story that
led to it.

What’s worst, in the paper or in the blackboard, an entirely correct proof
might have been produced in the wrong way, and you will never get a hint of
that just by looking at the final derivation tree that represents such a
proof. For instance, consider the usual derivation of the quantifier shift
that allows one to conclude that $(\forall x)(\forall y)P(x,y)$ and $(\forall
y)(\forall x)P(x,y)$ are equivalent formulas. Of course, to achieve your
initial goal what you should do is start by fixing a certain $y_{1}$ to
represent an arbitrary member of your universe of discourse and set as a new
goal the proof of $(\forall x)P(x,y_{1})$. Next, you fix an arbitrary $x_{1}$
and set as a new goal the proof of $P(x_{1},y_{1})$. So far you have invoked
two applications of a logical rule often called ‘$\forall$-introduction’.
Because you still need to prove $P(x_{1},y_{1})$ from $(\forall x)(\forall
y)P(x,y)$, two applications of ‘$\forall$-elimination’ will now do, if you
choose the obvious witnesses for the instantiations. Pick your preferred
proof-assistant and write the proof starting from the given, applying
$\forall$-elimination (twice) and then try applying $\forall$-introduction.
You will fail: the instances that you will produce are not ‘arbitrary’, but
only specific objects of your domain; you should not expect to generalize from
them.

However essential is dynamics to a proof, the standard theoretical treatises
on Proof Theory still choose to simply ignore it. Rather than defining proofs
as sequences of collections of derivations trees each with their own purpose
and history, a proof is commonly identified simply with the final derivation
tree that magically gather all the former trees into a whole. Most of the
movie has been lost in the process, as spectators just look at the final
credits in awe. Yet all practitioners know perfectly well that something
fundamental is missing.

### Playing and replaying proofs.

The last example in the previous discussion has already illustrated a common
feature of proof dynamics that is taken into account by a practitioner writing
a so-called proof script for a given conjecture: reasoning may proceed forward
from the givens or backwards from the goals. For instance, given two families
of sets, $\mathcal{F}$ and $\mathcal{G}$, a student might want to prove that
$x\in\bigcup\mathcal{F}$ follows from
$x\in\bigcup(\mathcal{F}\cap\mathcal{G})$. Now, reasoning backwards from the
initial goal, proving $x\in\bigcup\mathcal{F}$ means going through the so-
called ‘$\exists$-introduction’ rule, where the new goal would consist in
finding a witness $y\in\mathcal{F}$ such that $x\in y$. On the other hand,
using the hypothesis $x\in\bigcup(\mathcal{F}\cap\mathcal{G})$ means going
through the so-called ‘$\exists$-elimination’ rule, for in this case the
procedure, reasoning forward from the given, would consist in considering an
arbitrary element $z$ of $\mathcal{F}\cap\mathcal{G}$ such that $x\in z$. The
student will easily tie the two ends of the proof, of course, when she finds
out she might choose $y=z$.

“If you can’t solve a problem, then there is an easier problem you can solve:
find it.” (cf. [9]). Flexible proof assistants will typically allow you to
solve a problem by exploring proofs in both directions, forward and backwards,
to try and find that easier problem. Using an analogy from programming
language paradigms, proof languages used by proof assistants might come in a
declarative style that “resembles program source code more than mathematics”
or in a procedural style in which “one holds a dialogue with the computer”
(cf. [15]). For the obvious reasons, research efforts have been consistently
devoted to developing a mathematical vernacular for proof assistants (cf. [3])
that resembles the formal use of natural language found in mathematical
texts.222Mathematicians can be quite conservative, in fact, and even proposals
to the effect that an effort should be made to employ a more disciplined and
structured use of language (cf. [6]) have for the most part appeared to fell
on deaf ears. Isn’t this a whole lot of work just to end up with something
that appears as if it had been done with pencil-and-paper? Well, this is where
the analogy breaks down. Note indeed that proofs described as scripts in a
proof assistant can be executed like any program. That allows one, in
principle, to “describe not only what the machine should do, but also why it
should be doing it — a formal proof of correctness” (cf. [5]).

### More on the power of computer-inspired analogies.

Many a cognitive scientist has found a common denominator with defenders of
Artificial Intelligence in explaining the difference between the mind and the
brain in terms of an analogy to the difference between software and hardware.
Imperfect as any analogy, such an explanation will already allow for debates
to run, for instance, about the meaning and the roles of consciousness and
emotions in the resulting picture. More to the point, a little experience in
programming or some experience with proof assistants often help bringing forth
some more specific and useful analogies. For instance, a comparison that many
students find compelling is the one that equates the discharge of assumptions
and the discharge of parameters in certain natural deduction proofs to the
destruction of local variables, in imperative programming, when leaving the
scope of functions to which they belong, and that equates non-discharged
hypotheses to global variables of a program. For another example, the
familiarity with functions with type void, in programming, not rarely appears
to be advantageous to students striving to understand the interpretations of
nullary functions or nullary predicates.

Allegedly, a good education in Computer Science turns the apprentice more
prone to recognizing that many symbols for variables that appear in
mathematical expressions are actually bound to certain operators (such as
summations, limits or integrals), or are bound to hidden (universal)
quantifiers, and so they might usefully be thought of as standing as
placeholders that allow for certain kinds of syntactic reductions. From an
implementation viewpoint, the conceptual understanding of the role of binding
is in fact shared by computer scientists more often with linguists than with
mathematicians. On the same track, the insightful Curry-Howard correspondence
that maps propositions to types, proofs to programs, and proof simplification
strategies to program evaluation strategies tends to be better appreciated by
those who have been exposed to the compilation routines of modern programming
languages or proof assistants.

And here is a final note on the seductive power of analogy. As with any search
related to problem solving, one way of thinking about proof search is as
another example of disciplined activity that benefits from intelligent
guidance. Now, if one is still willing to defend that “intellectual activity
consists mainly of various kinds of search” (cf. [12]), then one should be
more than willing to build tools to let the students experiment with and
search for their own proofs, and invest on the partnership between students
and their ‘intelligent machinery’.

### When definitions apply [and when they do not].

There is no space here, nor is it my intention, to discuss the role of
definitions in the teaching and learning of mathematics. This has been done
with competence in [14], and elsewhere. The value of definitions that make
precise certain fundamental concepts should not be underestimated: It would
not be (much of) an exaggeration, for instance, to say that the whole of Logic
amounts simply to the study of a couple of capital definitions, namely, those
of the concepts of satisfaction, proof, computation, and valid reasoning.

For all that matters, and putting aside for a moment their cognitive role in
reasoning, I may here assume definitions to be dealt with through a simple
rewriting: definiens is allowed to replace definiendum, or vice-versa.
Assuming the student can process such rewritings while cleverly avoiding
circular reasoning, assuming that the student competently grasps the content
of the definitions she is supposed to work with, and also assuming that the
student can make such definitions part of her technical repertoire, it still
seems to me that insufficient emphasis is put on knowing what to do when a
defined term, operation or relation applies as well as when it does not apply
in the theory at hand. For instance, if set complement ($\setminus$) is
defined in the usual way, what does it mean to reason from a hypothesis of the
form $c\notin a\setminus b$? (novice students often have difficulty in
recognizing in this the conditional assertion ‘if $c\in a$ then $c\in b$’) For
a more important example, what does it mean for a statement not to follow from
a given set of hypotheses? Many students who claim to understand,
respectively, the notions of set complement and logical consequence still have
difficulty giving useful answers to the two previous questions.

Much of what has been noted as a problem about dealing with definitions
extends to dealing with identities (for which careless rewriting might in fact
easily turn out nonterminating). Universal statements concerning the failure
of certain identities are seldom used in theories that focus exclusively on
equational reasoning. For the interested reader, I recall though a nice
example of the possible use of inequalities, in combination with automated
proof search. Recall that a Robbins algebra is a structure containing a
commutative and associative binary symbol $+$ and a unary symbol ′ satisfying
the equation $(\forall x)(\forall
y)((x^{\prime}+y^{\prime})^{\prime}+(x^{\prime}+y)^{\prime})=x$. A
computerized proof that a Robbins algebra that contains an $+$-idempotent
element is Boolean was quickly found by supposing, by contradiction, the
denial of another equation which was known since 1933 to axiomatize the
variety of Boolean algebras. This result ended up representing a key step in
the proof, entirely uncovered by an automated prover, that all Robbins
algebras are Boolean, settling a problem that had been open for more than six
decades (cf. [7]).

### Finding the right balance between automation and our pedagogical purposes.

Are computerized proofs legible? And, to better start with, are they
informative? How much will the students learn from them? While the first
question might largely amount to a puzzle for semiotics, the last question
poses a challenge for educators. In the previous paragraph I have just
mentioned the ‘solution to the Robbins problem’. It should be noted that this
solution, which has resisted the attacks of generations of human provers, also
proved to be really hard for human checkers, for the substitutions required by
the use of the equations involved terms that were long and difficult to parse.
In this sense, the first computerized proofs that were automatically found
seemed too unstructured and did not contribute much in insight for their
intrepid human readers.

So much for fully automated proving. As we mentioned before, the languages
used by interactive proof assistants aim at being flexible, and often contain
‘tacticals’ or ‘methods’ that allow one to fine tune the amount of automation
one wants to introduce into the most bureaucratic or relatively boring steps
of a proof construction. In the case of large steps done with automation, many
proof assistants will allow one to inspect the structure of the proof object
that has been constructed by them, hidden from the users’ eyes. The students
directly involved in the very implementation of such tacticals or automated
provers will no doubt learn a lot from their service to the community.
However, novice students that abuse on proofs produced by a ‘blast’, followed
by a seeming miracle, often fail to see how such proofs relate to the problems
they have when confronted with the simplest mathematical conjectures. In that
sense, it would seem to me that, for pedagogical purposes, automation had
better be introduced in really small doses.

Of course, it all depends on what we intend to teach. Take the example of
classical propositional logic, and their usual analytic tableaux or sequent
systems. Both proof systems are capable of originating simple decision
procedures. However, if our purpose involves capitalizing on the conceptual
distinction between formal proofs and formal semantics, tableaux tend to
dangerously tread on the dividing line. Moreover, when done on pencil-and-
paper, the steps taken in the construction of tableaux are often left
unjustified, as if the derivation tree by itself would be straightforward to
decipher. Arguably, and that will surely depend on the way you teach them,
much more flexible systems based on sequents would also seem to pose some
difficulties related to the understanding of formal semantics. Many will
contend, in fact, that natural deduction is superior as a proof system that
allows students to more easily construct a conceptual map in between the way
they have been taught to formulate their mathematical reasoning using
regimented fragments of natural language and their conversations with the
machine. Not by chance, several interactive proof assistants in the market do
make use of some variety of natural deduction in their metalanguage. All in
all, if I may insist, assuming the chosen purpose of teaching structured
mathematical thinking, the motto should be: ‘Less automation Is More’.

### On the role of proof strategies.

Some proof systems are so robust that proofs written in them are bound to
terminate (by confirming or by refutating of a given conjecture) no matter how
you proceed in developing them. The odd worst-case scenario for usual analytic
tableaux for classical propositional logic, for instance, is known to be much
more costly than truth-tables, but if you persist long enough in decomposing
your hypotheses, you will exhaust any tableau, no longer being able in fact to
further extend its branches by the addition of new data. The first-order case,
as it should be clear, is quite different in that respect: Already in the
examples we presented in the above paragraphs, interchanging the order in
which the quantifier rules were applied could easily lead to failed attempts
at producing a proof.

Some other proof systems will only work well with a lot of external help. For
many decidable modal logics, for instance, some of the best proof systems
available need loop-checkers to put an end to their proof-search procedures
(cf. [8]). Some classic-like tableaux for many-valued propositional logics
—all such logics being obviously decidable— will only be assured to produce
terminating proofs if you abide to certain proof strategies (cf. [1, 2]). Here
again there would seem to be a task for proof-theorists: The lesson concerning
the importance of employing proof strategies is in fact general enough to
suggest that a proof system should always be presented associated to certain
proof heuristics — even when the choice of such heuristics turns out not to
affect the use of the system in actually designing successful derivations.

Designing a proof system that only allows its user a very small number of
options for the construction of her proofs is often a poor and unrealistic
alternative. Equipping the user with variegated tools-for-thought and proof
techniques seems much more advisable. If this generous education process is
carried out wisely, then much longer after the student has completely
forgotten what she has once proven she might still know how to approach new
(or the same old) problems, and go about solving them. The student had better
learn how to construct a mathematical argument for a direct proof, an
existential one, proofs by reduction, by contraposition or by cases, learn the
essential forms of induction, learn the basic useful combinatorial principles.
And she should learn how to refute a conjecture by a counter-example along
with its corresponding step by step justification. What exactly she happens to
end up proving, as long as it meets her professed goal, is often less
important than the increased expertise acquired by her in employing the
appropriate strategies towards accomplishing the task at hand.

##  3\. A case study: the TryLogic

We here briefly assess a tool that embodies some of the above discussed
teaching principles. Its design was based on a number of preexisting tools,
following the IMS interoperability standards for distributed learning333See
http://www.imsglobal.org/lti/index.html., and may be integrated as an external
tool to any Virtual Learning Environment444We happened to use Moodle
(https://moodle.org/) to that purpose.. A major interactive theorem
prover555We have used a standard formal theory for natural deduction
implemented in Coq (https://coq.inria.fr/), to which I have added primitive
rules for bi-implication, and we implemented in Coq also a refutation theory
for reasoning with the notion of satisfaction in formal semantics. is used by
our tool through the ProofWeb interface666We have in fact installed our own
ProofWeb (http://proofweb.cs.ru.nl/) local server, and extended it to
correctly display the trees from both our full natural deduction theory and
our refutation theory.. Finally, students are intended to learn how to use the
system exclusively through the TryLogic777Our system is available at
http://lolita.dimap.ufrn.br/trylogic. system, an infrastructure consisting of
an interactive tutorial, based on a successful online system for teaching
programming languages888See http://try.ocamlpro.com/.. Students have common
access to a number of exercises to practice their skills with natural
deduction, and typically they will receive directly in their areas a number of
personalized exercises concerning: randomly chosen challenges involving
carefully handcrafted conjectures to be proven; computer-generated exercises
involving conjectures to be refuted; a number of computer-generated challenges
in which they are not told whether the corresponding conjectures should be
proven, or else refuted. The latter two groups of propositional-level
exercises are produced by a tool999The Conjectures Generator is available at
http://lolita.dimap.ufrn.br/logicamente-ge/, with open source code available
at http://github.com/terrematte/logic-propgenerator. implemented over the SAT-
solver Limboole101010Available at http://fmv.jku.at/limboole/..

In my understanding, the whole process of writing proof scripts with the help
of a proof assistant helps the students see proofs as instructions to be
executed in order to dynamically explore a problem-solving challenge, even if
that does not perfectly match the static proof-theory that they learn from the
mathematical textbooks. The difficulty of the task, in which we strictly
control the amount of automation that we allow the students to use, makes them
ponder about how useful it may be to entertain a strategical approach to a
given challenge, and the nature of the task and the easy interaction with and
responsiveness of the underlying media encourages them to do some heuristic
exploration through trial and error.

Before TryLogic, our group had invested for a few years on the Logicamente
(cf. [11]), a growing collection of Learning Objects combined with the
respective learning scripts, expositions, tasks and activities on subjects of
Logic. The latter suite of tools was largely independent from other existing
tools, and was developed ab nihilo through the collaborative effort of
students that got involved in the project and were evaluated by their
contributions to it. My impression about the project Logicamente, as fun as it
might have been to work on, is that it was much more successful, from a
pedagogical viewpoint, for the students that implemented its modules than for
other students who used these modules later on. I am not trying now to sell
TryLogic (and its associated tools) to you, even though I would be delighted
if you bought it (and it is free of cost). What I feel to be really important
about this new project (which we report upon in more detail in [10]) is that
it is entirely based on exploring the teaching principles discussed in the
previous section, for whose convenience and effectiveness I do not intend to
offer here independent evidence except for the fact that a few dozen students
have had very fruitful interactions with TryLogic along the last three years.

## Coda

The critical transition from high school to higher education has —and with a
good reason— received increased attention from educators worldwide. Two
distinct paths might be taken by in individual undergoing post-secondary
education, namely: focusing on technical content that adds to know how, or
investing on a scientific education that presupposes a frame of mind not
dispensing with the know why. It has been eloquently argued elsewhere that
Logic has a secure role in teaching proof and that this would be better
promoted by emphasizing general principles leading to deeper understanding,
rather than by focusing on concrete narrow problem-solving strategies; more
generally, teaching logical reasoning “builds students’ confidence in the
rationality of the mathematical enterprise and helps allay their fear of
failure” (cf. [4]).

All education starts from personal reflections. The present paper has
collected my own reflections, at the present date, on the topic of ‘tools for
teaching logic’, and what we can learn from and with such tools. Scientific
discussions concerning education, though, cannot end at the level of
intuition. We need data.

In the above I have proposed that Proof Theory should redefine proofs as
dynamical objects, have argued about the advantages of treating proofs as
executable code, and of testing the understanding of definitions by inquiring
about the conditions in which they fail to apply, have commented upon the
contributions given by certain computer-inspired analogies, and finally I have
briefly discussed the importance of exercising one’s mathematical thinking by
acquiring a number of skills polished by the intelligent use of proof
strategies. We should always aim at achieving maximal pedagogical effect. The
best way of measuring this, however, is probably not by bragging about how
well the students succeed in the tasks we assign them with our own tools and
measure with our own rulers, but by their later performance in other tasks
that demand similar competences. Still, data needs to be collected to test
whether our teaching principles are sound and far-reaching.

If arguments aim at convincing, the same effect may be achieved ad baculum. We
had better not teach our students to resort to sticks, though. Many novice
students have serious trouble telling the difference betweeen a proof and,
say, a broccoli plantation. Talent and experience are needed for recognizing
both successful and failed proofs. In the same way that you should not dare
teaching formal grammar to a student that is still being alphabetized, I
believe that students had better be repeatedly exposed to real-world proofs
before you endeavor teaching them formal logic and proof techniques. The
particular tool I have described in the previous section was introduced in
blended learning, and used concepts of Cognitive Load Theory in its
instructional design. I tend to believe, however, that the teaching principles
discussed in this paper can —and should— be carried over to corresponding
theoretical investigations, as well as to other tools and learning theories.

## References

  * [1] Carlos Caleiro and João Marcos.  Classic-like analytic tableaux for finite-valued logics.  In Proceedings of WoLLIC 2009, volume 5514 of LNAI, pages 268–280. Springer, 2009.
  * [2] Carlos Caleiro, João Marcos, and Marco Volpe.  Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics.  To appear in _Theoretical Computer Science_ , preprint available at http://arxiv.org/abs/1408.3775, 2015.
  * [3] Nicolaas G. de Bruijn.  The mathematical vernacular, a language for mathematics with typed sets.  In P. Dybjer et al., editor, Proceedings of the Workshop on Programming Languages, pages 865–935. Marstrand, Sweden, 1987.
  * [4] Susanna S. Epp  The Role of Logic in Teaching Proof  _The American Mathematical Monthly_ , 110(10): 886–899, 2003.
  * [5] Georges Gonthier.  Formal proof — The Four-Color Theorem.  Notices of the AMS, 55(11):1382–1393, 2008.
  * [6] Leslie Lamport.  How to write a 21st century proof.  Journal of Fixed Point Theory and Applications, 11(1):43–63, 2012\.
  * [7] William McCune.  Solution of the Robbins problem.  Journal of Automated Reasoning, 19(3):263–276, 1997.
  * [8] Sara Negri.  Proof analysis in modal logic.  Journal of Philosophical Logic, 34:507–544, 2005.
  * [9] George Pólya.  Mathematical Discovery: On understanding, learning, and teaching problem solving, volume I.  Wiley, 1962.
  * [10] Patrick Terrematte and João Marcos.  TryLogic tutorial: An approach to learning logic by proving and refuting.  4th International Conference on Tools for Teaching Logic, pages 233–241.
  * [11] Patrick Terrematte, Fabrício Costa, and João Marcos.  Logicamente: A Virtual Learning Environment for logic based on Learning Objects.  In TICTTL 2011, volume 6680 of Lecture Notes in Artificial Intelligence, pages 223–230. Springer, Berlin, 2011.
  * [12] Alan M. Turing.  Intelligent machinery.  Technical report, National Physical Laboratory, 1948.  22 pages.
  * [13] Daniel J. Velleman.  How to Prove It: A structured approach.  Cambridge University Press, 2nd edition edition, 2006.
  * [14] Shlomo Vinner.  The role of definitions in the teaching and learning of mathematics.  In David Tall, editor, Advanced Mathematical Thinking, volume 11 of Mathematics Education Library, pages 65–81. Springer, 1991\.
  * [15] Freek Wiedijk.  Formal proof — Getting started.  Notices of the AMS, 55(11):1408–1414, 2008.


# High-Field Microscale NMR Spectroscopy with NV Centers in Dipolarly-Coupled
Samples

Carlos Munuera-Javaloy  Department of Physical Chemistry, University of the
Basque Country UPV/EHU, Apartado 644, 48080 Bilbao, Spain  EHU Quantum Center,
University of the Basque Country UPV/EHU, Leioa, Spain  Ander Tobalina
Department of Applied Mathematics, University of the Basque Country UPV/EHU,
01006 Vitoria-Gasteiz, Spain  EHU Quantum Center, University of the Basque
Country UPV/EHU, Leioa, Spain  Arquimea Research Center, 38320 La Laguna,
Spain  Jorge Casanova  Department of Physical Chemistry, University of the
Basque Country UPV/EHU, Apartado 644, 48080 Bilbao, Spain  EHU Quantum Center,
University of the Basque Country UPV/EHU, Leioa, Spain

###### Abstract

Diamond-based quantum sensors have enabled high-resolution NMR spectroscopy at
the microscale in scenarios where fast molecular motion averages out dipolar
interactions among target nuclei. However, in samples with low-diffusion,
ubiquitous dipolar couplings challenge the extraction of relevant
spectroscopic information. In this work we present a protocol that enables the
scanning of nuclear spins in dipolarly-coupled samples at high magnetic fields
with a sensor based on nitrogen vacancy (NV) ensembles. Our protocol is based
on the synchronized delivery of radio frequency (RF) and microwave (MW)
radiation to eliminate couplings among nuclei in the scanned sample and to
efficiently extract target energy-shifts from the sample’s magnetization
dynamics. In addition, the method is designed to operate at high magnetic
fields leading to a larger sample thermal polarization, thus to an increased
NMR signal. The precision of our method is ultimately limited by the coherence
time of the sample, allowing for accurate identification of relevant energy
shifts in solid-state systems.

##  I Introduction

During the last decade, the so far most productive leg of quantum technologies
Dowling03 , namely, quantum sensing Degen17 , has produced magnetometers able
to detect ever weaker fields. Such development has had a deep impact in the
realm of nuclear magnetic resonance (NMR) Levitt08 , a field that, despite its
unquestionable success, has limitations due to the inherent weakness of target
signals necessitates the scanning of millimeter-sized samples. Nitrogen
vacancy (NV) centers in diamond Doherty13 , however, reported the detection of
signals from smaller samples leading to NMR experiments with unprecedented
spatial resolution. NV centers stand out for their capacity to operate at room
temperature leading to smaller, and easier to operate magnetometers compared
to platforms that require stringent conditions such as, e.g., superconducting
quantum interference devices (SQUIDs).

NMR spectroscopy reveals frequency shifts relative to a base Larmor frequency
which encode structural information about sample molecules as well as of their
surrounding environment. In this scenario, one of the most impressive results
produced by NV based NMR sensors –enabled by heterodyne protocols that
overcome the resolution boundary posed by the coherence time of the NV centers
Boss17 ; Schmitt17 – is the record of spectral features from picoliter volume
samples with high-resolution Glenn18 . Nevertheless, in thermally polarized
samples, these protocols require a high nuclear spin concentration (typically,
highly protonated samples) and a significant number of repetitions to obtain
meaningful results. A possibility for detecting samples at lower
concentrations and achieving more competitive protocols is to hyperpolarize
the samples in a previous step Arunkumar21 ; Bucher20 . In addition,
performing the experiment at high fields directly provides higher polarization
rates while it facilitates the extraction of relevant information from the
recorded spectra, as chemical shifts increase and J-couplings become clearer
Ugurbil03 . Although NV-NMR spectroscopy at high fields has not yet been
experimentally demonstrated, recent proposals have introduced protocols that
enable the acquisition of high-resolution spectra in strong external magnetic
fields Munuera23 ; Meinel23 ; Alsina23 . In particular, our proposal AERIS
Munuera23  operates encoding the target nuclear energy shifts in the amplitude
variation of the sample’s longitudinal magnetization which oscillates at a
tunable rate –i.e., at a slow rate of, typically, tens of KHz even at large
fields– during consecutive detections. Recent publications indicate that the
experimental implementation of AERIS is just a matter of time Daly23 .

An important limitation of state-of-the-art NV-NMR spectroscopy is caused by
the strong dipolar coupling among target nuclei, which results in intricate
spectra that challenge data interpretation. This becomes especially critical
in solid-state material research, where homonuclear dipole-dipole interactions
hinder subtler couplings (heteronuclear interactions are less challenging as
they can be eliminated by driving only one of the species). The NMR community
has dedicated significant efforts to mitigate the impact of dipolar
interactions Madhu16 , and today solid-state NMR spectroscopy is extensively
used in distinct research areas: In pharmaceutics it characterizes active
pharmaceutical ingredients (APIs) and their interaction with excipients
(inactive substances added to a drug that serve various purposes such as
binding or preserving the API) Pisklak14 ; Pisklak16 ; Nie16 , among many
other applications (see Marchetti21  for an extensive review on the topic). In
epidemiology, it provides key insights of the structure of molecules related
with diseases as present in our societies as Alzeimer Tycko11 . In energy
storage research is used to characterize the local structure of solid
materials used in batteries and fuel cells Pecher17 .

These areas, along with many others, would largely benefit form sensors able
to produce narrower spectral lines from smaller solid-state samples. NV-NMR
spectroscopy emerges as the prominent technique to access samples in the
microscale regime, however, it remains limited to the liquid state scenario
where the dipole-dipole interactions get naturally averaged out due to fast
molecular motion, leaving a plethora of relevant applications out of its range
of action.

Figure 1:  (a) Relative positions of axis $A$ (clear-blue), $\bar{A}$ (dark-
blue), $B$ (clear-magenta), $\bar{B}$ (dark-magenta). The motion of the
magnetization inbetween LG4 blocks ($A\bar{A}\bar{B}B$) is shown in purple.
This evolution is described as a rotation in the plane (in yellow)
perpendicular to the $C$ axis in accordance with the effective Hamiltonian in
Eq. (4) for a single $\delta_{i}^{*}$. (b) (Top) Magnetization rotations
during each of the four RF drivings. (Bottom) Projection of the magnetization
onto $\hat{z}$ as it rotates during a full LG4 block. This projection
determines the magnetic signal for the NV ensemble sensor.

In this work, we devise a protocol that overcomes these limitations and
enables high resolution NV-NMR spectroscopy of ordered samples with strong
homonuclear dipolar coupling at elevated external magnetic fields, allowing to
take advantage from the higher polarization rates and stronger chemical
shifts. Our protocol features the delivery of two radiation channels –radio-
frequency (RF) and microwave (MW)– synchronized with measurements on an NV
ensemble magnetometer. The RF channel drives the sample with a twofold
purpose. On the one hand it effectively decouples the target nuclear spins,
diminishing the effect of strong homonuclear couplings in the recorded
spectra, and enabling the obtention of nuclear energy shifts. Remarkably, the
decoupling benefits from increasing RF intensities could be specially
effective in the small volume regime, where current RF antennas have reported
nuclear spin rotation velocities within the range of tens to hundreds of kHz
Herb20 ; Yudilevich23 . On the other hand, the RF bridges the interaction
among NV sensors and fast rotating nuclear spin by generating a slow-frequency
NMR signal trackable by the NV sensor. Simultaneously, the MW channel delivers
a tailored pulse sequence to the NV ensemble enabling the detection of the
magnetic field emitted by the driven sample. This sequence is interspersed
with measurements of the sensor’s state to construct the spectra in a
heterodyne frame leading to a spectrum only limited by the nuclear sample
coherence. Finally, we provide analytical expressions that map the detected
resonances with target energy shifts.

##  II The Method

###  II.1 RF modulation of nuclear spins

Lee and Goldburg (LG) showed in a seminal paper Lee65  that an off-resonant
continuous RF field cancels, up to first order, the contribution to the
nuclear spin dynamics of homonuclear dipole-dipole interactions if the LG
condition $\Delta=\pm\Omega/\sqrt{2}$ holds. Here,
$\Delta=\omega_{L}-\omega_{d}$ is the detuning between the carrier frequency
of the RF driving field ($\omega_{d}$) and the Larmor precession of the spins
($\omega_{L}$), and $\Omega$ is the Rabi frequency of the RF driving.
Subjecting a spin ensemble to an off-resonant RF field leads to collective
nuclear spin rotations along an axis tilted with respect to $\hat{z}$ (the
direction of the static magnetic field). More specifically, the tilted axis
–in the following $P$– has a component
$\frac{\Delta}{\sqrt{\Omega^{2}+\Delta^{2}}}$ along $\hat{z}$, while its
projection on the orthogonal $xy$ plane is
$\frac{\Omega}{\sqrt{\Omega^{2}+\Delta^{2}}}$.

Further developments have built upon the original LG sequence demonstrating
the ability to remove higher order contributions of the dipole-dipole
interaction, thus leading to even narrower spectral lines. Prominent examples
are the frequency-switched (FSLG) Waugh72  and phase-modulated (PMLG)
Vinogradov99  versions of the original LG sequence. Our protocol incorporates
the advanced LG4 sequence Halse13  over nuclei, which exhibits remarkable
decoupling rates and enhanced robustness against RF control errors. The LG4
consists on concatenated blocks of four consecutive off-resonant RF drivings,
all complying with the LG condition, leading to rotations along four different
axes. This is, the rotation axis $P$ alternates among $A,\bar{A},\bar{B}$ and
$B$, whose relative positions are illustrated in Fig. 1 (a). Note that, at
each block, nuclear spins undergo two sets of complementary rotations along
axis pointing in opposite directions ($A,\bar{A}$ and $B,\bar{B}$).

The nuclear spin Hamiltonian during each individual rotation of the LG4
sequence reads (see Appendix A)

$H=\sum_{i=1}^{N}\left(\frac{\pm\delta_{i}}{\sqrt{3}}+\bar{\Omega}\right)I^{i}_{P},$
(1)

where $\delta_{i}$ is the target nuclear shift of the $i$th spin (its sign
depends on the direction of the rotation, positive value $``+\delta_{i}"$ is
assigned to rotations along $A$ and $B$, and the negative value
$``-\delta_{i}"$ to rotation along $\bar{A}$ and $\bar{B}$),
$\bar{\Omega}=\sqrt{\Delta^{2}+\Omega^{2}}$ is the effective Rabi frequency,
and the spin operator $I^{i}_{P}$ takes one of the following forms

$\displaystyle I^{i}_{A}$ $\displaystyle=$ $\displaystyle\left(\Omega
I^{i}_{x}\sin{\alpha}+\Omega I^{i}_{y}\cos{\alpha}+\Delta
I^{i}_{z}\right)/\bar{\Omega},$ $\displaystyle I^{i}_{\bar{A}}$
$\displaystyle=$ $\displaystyle-I^{i}_{A},$ $\displaystyle I^{i}_{B}$
$\displaystyle=$ $\displaystyle\left(-\Omega I^{i}_{x}\sin{\alpha}+\Omega
I^{i}_{y}\cos{\alpha}+\Delta I^{i}_{z}\right)/\bar{\Omega},$ $\displaystyle
I^{i}_{\bar{B}}$ $\displaystyle=$ $\displaystyle-I^{i}_{B}.$ (2)

According to the LG4 scheme Halse13 , the phase of the driving is set to
$\alpha=55^{\circ}$ to minimize the line-width of the resonances.

Note that in Eq. (1) we assume that the internuclear interaction Hamiltonian
$H_{\rm nn}=\sum_{i>j}^{N}\frac{\mu_{0}\gamma^{2}_{n}\hbar}{4\pi
r_{i,j}^{3}}\bigg{[}\vec{I}_{i}\cdot\vec{I}_{j}-3(\vec{I}_{j}\cdot\hat{r}_{i,k})(\vec{I}_{j}\cdot\hat{r}_{i,j})\bigg{]}$
can be neglected due to the introduced decoupling sequence. This assumption
simplifies the subsequent analysis. However, $H_{\rm nn}$ will be taken into
account in the numerical model in Sec. III.

In the remainder of this section, we analyze the signal emitted by the sample
subjected to the RF decoupling fields and develop analytical expressions for
the target energy shifts.

The magnetic field that originates from the sample during the nuclear spin
rotation produced by each RF field of the LG4 follows the general form

$s(t)=\Gamma\cos{(\bar{\Omega}t+\phi)}+b.$ (3)

Hereafter, we often refer to $s(t)$ as the signal, as it constitutes the
target field for the NV ensemble sensor. In fact, its amplitude $\Gamma$,
phase $\phi$, and static bias $b$ depend on the configuration of the nuclear
spin ensemble and thereby on the $\delta_{i}$ energy shifts (see Appendix C),
so detecting and properly reading $s(t)$ enables to unravel the desired
information.

Consequently, the LG4 meets a twofold goal. Namely: (i) It results in a
nuclear spin dynamics with minimal effect from the dipole-dipole interaction
(see Appendix A for the full derivation of the Hamiltonian in Eq. (1)),
enabling the identification of the weaker but interesting $\delta_{i}$ shifts.
(ii) It induces a tunable rotation speed in the sample ($\propto\bar{\Omega}$,
see Eq. (3)), facilitating the interaction between nuclear spins and the NV
ensemble sensor even at high external magnetic fields. Regarding point (ii),
it is important to note that without using RF drivings on the sample, standard
techniques based on imprinting in the NVs a rotation speed comparable to the
nuclear Larmor frequency would necessitate the application of unrealistic MW
fields. For context, in a magnetic field of approximately 2.35 Tesla, hydrogen
spins rotate at a speed of $(2\pi)\times 100$ MHz, producing a signal hardly
trackable by an NV ensemble sensor operating with conventional methods.
Glenn18 ; Bucher20 ; Arunkumar21 .

Now, we examine the effects of RF decoupling fields in greater detail. Each RF
driving (leading to the rotations along $A,\bar{A}$, $B,\bar{B}$) is applied
for an interval $T=1/\bar{\Omega}$. Consequently, the total signal emitted by
the sample is a composite of distinct sinusoidal functions, condensed in Eq.
(3), each persisting for a duration $T$. Figure 1 (b) presents an illustrative
example of $s(t)$ by showing the rotation of a single magnetization vector
(associated with a specific $\delta_{i}$) around axes $A$, $\bar{A}$, $B$ and
$\bar{B}$.

Interestingly, with this RF control, the nuclear spins governed by Eq. (1)
would perform a complete turn at each RF driving, constantly returning to
their initial configuration if it were not for the $\delta_{i}$ shifts. These
shifts slightly alter the nuclear spin state (i.e., the sample magnetization),
thus imprinting a slower motion within the sample. More specifically, the
sample magnetization at the end of each LG4 block is determined by a set of
energy shifts $\delta^{*}_{j}$ (distinct from $\delta_{i}$) according to the
effective Hamiltonian (for details see Appendix A):

$H_{\rm eff}=\sum_{i}\delta^{*}_{i}I^{i}_{C},$ (4)

where $I^{i}_{C}$ is a spin operator along an axis $C$ that bisects $A$ and
$B$, see Fig. 1 (a), while

$\delta_{i}^{*}=\delta_{i}\frac{\sqrt{1+2\cos^{2}{\alpha}}}{3}.$ (5)

In summary, this section demonstrates that each LG4 block alters the sample
magnetization $\vec{M}$ through rotations along the $C$ axis, as depicted in
Fig. 1 (a). Moreover, we elucidate the mechanism governing the evolution of
$\vec{M}$ through the effective Hamiltonian outlined in Eq.$\eqref{eq: Heff}$,
while Eq. (5) establishes analytical expressions connecting the rates of the
effective rotations, $\delta^{*}_{i}$, with the target nuclear shifts
$\delta_{i}$.

In the next section we outline the protocol to monitor this effective
precessions with the NV ensemble sensor and extract the desired $\delta_{i}$
energies from its recordings.

###  II.2 Harvesting nuclear spin parameters with the NV ensemble

####  II.2.1 Geometrical interpretation of the phase accumulation

The target magnetic field over the NV ensemble sensor is a concatenation of
the sinusoidal signals in Eq. (3) (see lower panel in Fig. 1(b)). A particular
RF field at the $k^{\text{th}}$ LG4 block (note that, the accumulative
character of the rotations imposed by Eq. (4) make it crucial to identify the
number of the block from now on), produces a nuclear spin rotation around a
certain axis ($A$, $\bar{A}$, $B$ or $\bar{B}$) where the amplitude
$\Gamma_{k}$ of the resulting signal
$s_{k}(t)=\Gamma_{k}\cos{(\bar{\Omega}t+\phi_{k})}+b_{k}$ is directly
proportional to $\vec{M}_{k}^{\perp}$ (i.e., to the magnetization component
which is orthogonal to the rotation axis –$A$, $\bar{A}$, $B$ or $\bar{B}$– at
the start of each RF driving), and the phase $\phi_{k}$ corresponds to the
angle between $\vec{M}_{k}^{\perp}$ and $\hat{z}^{\perp}$. The latter is the
component of $\hat{z}$ that lies on the plane perpendicular to the rotation
axis. See the lower panel in Fig. 2 (a) and Appendix C for more details.

We now use this geometric description to analyze the phase accumulated by each
NV in the ensemble sensor when subjected to a generic pulse sequence. For this
analysis, we choose a standard Carr-Purcell-Meiboom-Gill (CPMG) sequence
Purcell46 ; Meiboom58 . In order to keep the discussion accessible, we focus
on the signal produced by the nuclear spins rotating around $A$ and limit
ourselves to an scenario involving a single effective energy shift,
$\delta_{i}^{*}$. Note, however, that the following results and the consequent
conclusions are valid for signals produced by nuclear spins rotating around
axes $B$, $\bar{A}$ and $\bar{B}$ and in situations involving multiple shifts.

The phase accumulated by an NV center interacting with the signal $s_{k}(t)$
and subjected to the CPMG sequence reads (see Appendix B)

$\Phi=\frac{4|\gamma_{e}|}{\bar{\Omega}}\Gamma_{k}\cos{\left(\phi_{k}\right)}.$
(6)

Hence, the phase accumulated by each NV is proportional to the projection of
$\vec{M}_{k}^{\perp}$ onto $\hat{z}^{\perp}$, or, in other words, to the
quantity $\Gamma_{k}\cos{\left(\phi_{k}\right)}$. The lower panel of Figure 2
(a) provides a clarifying (probably most needed) graphic explanation.

Figure 2:  (a) Illustration of a CPMG pulse block (upper panel) and its
geometric interpretation (lower panel). This panel shows a projection of the
sphere in Fig. 1 (b) viewed in a direction parallel to axis $A$. This view
facilitates the representation of the projections onto the plane perpendicular
to A of (i) The magnetization vector, denoted as $\vec{M}_{k}^{\perp}$, and
(ii) The $\hat{z}$ axis, referred to as $\hat{z}^{\perp}$. In addition, it
shows the trajectory followed by a magnetization vector during a rotation
around $A$ (purple circle) and after successive LG4 blocks (yellow ellipse).
(b) Upper panel, pulse block of our tailored sequence where the initial $\pi$
pulse is delivered at a time $t_{1}$. With this control, the phase
accumulation of the NV is proportional to the projection of
$\vec{M}_{k}^{\perp}$ onto $\hat{l}$ (shown in red), an axis tilted away from
$\hat{z}^{\perp}$ and aligned with the major axis of the yellow ellipse for
optimal contrast. (c) Evolution of the projection of $\vec{M}_{k}^{\perp}$
onto axis $\hat{z}^{\perp}$ (red) and onto axis $\hat{l}$ (blue). The
amplitude of the projection onto $\hat{l}$, resulting from the sequence in
panel (b), reaches the maximum value of 1. As the phase accumulated by the NV
is directly proportional to this projection, the timing of the pulses in (b)
ensures the maximum phase accumulation amplitude. Figure 3:  (Top) General
layout of our protocol containing the RF control over nuclear spins and the MW
pulse sequence on the NV ensemble. The magnetic field emitted by the nuclei as
a consequence of the RF rotations is depicted in light purple. As time
progresses, this field changes its shape, which changes the phase accumulated
by the NV, while MW pulses keep always the same structure. (Bottom) Evolution
of the expected results for the measurement over the NVs as the experiments
progresses, showing a sinusoidal pattern with frequency $\delta^{*}$. In the
presence of additional shifts, the measurement outcomes evolve as a sum of
sinusoidal components with corresponding frequencies $\delta^{*}_{i}$, which
can be extracted through Fourier transform analysis.

With this description in mind we can summarize the phase acquisition stage as
follows: The response of the NV centers to the signal emitted by the sample is
determined by the initial sample magnetization. As the protocol advances, the
magnetization vector precesses around $C$ with an angular velocity
$\delta^{*}_{i}$ as described by Eq. (4). In the orthogonal plane with respect
to $A$, this precession translates into an elliptical motion of the vector
$\vec{M}_{k}^{\perp}$, shown as a yellow ellipse in Fig. 2 (a). Thus, the
projection of $\vec{M}_{k}^{\perp}$ onto the $\hat{z}^{\perp}$ axis, and
consequently the phase accumulated by the NV in successive blocks of the LG4,
follow a sinusoidal function with frequency $\delta^{*}_{i}$. The resulting
expected value of the $\sigma_{z}$ operator of each NV in the ensemble at the
$k^{\text{th}}$ LG4 block (after applying a final $\pi/2$ pulse to transform
accumulated phase into populations), generalized to every $\delta_{i}^{*}$,
reads:

$\langle\sigma_{z}\rangle_{k}\approx
3D_{0}\sum_{i}\rho_{i}\cos{\left(\frac{4\delta_{i}^{*}k}{\bar{\Omega}}+\nu_{0}\right)},$
(7)

where $\rho_{i}$ is the spin density of the $i$th nucleus, $D_{0}$ is
detemined by the pulse sequence and $\nu_{0}$ depends on both the pulse
sequence and the initial nuclear state. A formal derivation of (7) as well as
further details can be found in Appendix C. The $0$ subindex in Eq. (7)
indicate that all parameters correspond to the reference CPMG sequence (note
that, in the next section we derive an improved sequence). Thus, the NV
response enclosed in Eq. (7) consists on a sum of sinusoidal functions that
encode the different $\delta_{i}^{*}$ which can be then extracted via standard
Fourier transform. Finally, $\delta_{i}$ targets can be obtained via a direct
application of Eq. (5).

####  II.2.2 Sensing MW pulse sequence

With the geometrical understating developed in the previous section, now we
present a tailored MW sequence to optimally detect the target $\delta_{i}$
shifts. This sequence retains a CPMG-like structure composed by two $\pi$
pulses spaced by $T/2$ to mitigates noise effects, $T$ being the CPMG block
length. Nonetheless, we adjust the timing of the pulses, see Fig. 2 (b), in
particular the time at which the first pulse is applied ($t_{1}$ hereafter).
Consequently, the phase accumulated by each NV in the ensemble sensor (recall
that we are focusing on the signal produced by the nuclear spins rotating
around $A$) reads

$\Phi=\frac{4\Gamma_{k}|\gamma_{e}|}{\bar{\Omega}}\cos{\left(\phi_{k}-\varphi\right)}.$
(8)

In our geometrical framework, adjusting the timing of the pulses results in an
accumulated phase proportional to the projection of $\vec{M}_{k}^{\perp}$ onto
an axis $\hat{l}$, which is tilted at an angle
$\varphi=\frac{\pi}{2}-\bar{\Omega}t_{1}$ relative to $\hat{z}^{\perp}$ (see
Fig. 2 (b)).

The ability to pivot the axis in which $\vec{M}_{k}^{\perp}$ gets projected
(note this can be done by selecting distinct values for $t_{1}$ since
$\varphi=\frac{\pi}{2}-\bar{\Omega}t_{1}$) allows us to design a pulse
sequence that maximizes contrast in the recorded spectra. From block to block,
$\vec{M}_{k}^{\perp}$ evolves following an ellipse, therefore, we design the
pulse sequence so that the phase accumulated by each NV is proportional to the
projection of $\vec{M}_{k}^{\perp}$ into the major axis of the elipse. By
doing so, the projecting axis and the direction that contains the extreme
points of the elliptic path of $\vec{M}_{k}^{\perp}$ match, thereby yielding
the maximum amplitude in the oscillation of $\Phi$ in successive blocks, see
Fig. 2 (b). In particular, this is achieved by setting
$\varphi=\arccos{\frac{\sqrt{3}\cos{\alpha}}{\sqrt{2+\cos{2\alpha}}}}$, which
determines the timing of the pulses as $t_{1,A}\approx 0.14\,T$ for optimal
detection of the signal produced by the nuclear spins rotating around $A$.
Repeating the same analysis for the signals produced by nuclear spin rotations
around $\bar{A}$ and $\bar{B}$ we find $t_{1,{\bar{A}}}=\frac{T}{2}-t_{1,A}$
and $t_{1,{\bar{B}}}=t_{1,A}$.

Summing up, our tailored MW pulse sequence is separated in blocks. Each block
contains two $\pi$ pulses specifically timed to optimally detect the signal
produced by the corresponding RF field. To maintain synchrony between the two
control channels (MW and RF) and to avoid turning off the nuclear decoupling
field, the sensor is measured and reinitialized while the RF field is on.
Figure 3 shows the general layout of our protocol, including the drivings over
the sample and the sensor, and showing the evolution of the expected outcomes
in successive measurements, which read

$\langle\sigma_{z}\rangle_{k}\approx 3D_{\rm
opt}\sum_{i}\rho_{i}\cos{\left(\frac{4\delta_{i}^{*}k}{\bar{\Omega}}+\nu_{\rm
opt}\right)},$ (9)

where $D_{\rm opt}\approx 1.1D_{0}$ (i.e., with the tailored MW sequence the
contrast increases a $10\%$) and $\nu_{\rm opt}=0$ which corresponds to a
initial sample magnetization oriented along the axis perpendicular to the $A$
and $B$ axes, achieved by a RF pulse that triggers the protocol. Finally, we
access the effective frequencies $\delta_{i}^{*}$ by Fourier transforming the
recorded data and obtain the target $\delta_{i}$ shifts from Eq. (5).

##  III Results

Figure 4:  Spectra obtained from three simulations with RF Rabi frequencies of
$(2\pi)\times$100 kHz (yellow line), $(2\pi)\times$150 kHz (blue line), and
$(2\pi)\times$200 kHz (red line). Vertical dashed gray lines indicate the
expected resonances, i.e. the two $\delta^{*}_{i}$, of approximately 140 Hz
and 45 Hz. For comparison, a spectrum obtained with AERIS is depicted (black
line), using an RF Rabi frequency of $(2\pi)\times$150 KHz. In all
simulations, the nuclear sample starts in a thermal state corresponding to a
temperature of T=300 K in an external magnetic field of 2.1 T. The sample
evolves for a total time of 0.5 s.

We test our protocol by simulating its implementation to detect the chemical
shifts of hydrogen nuclear spins in ethanol molecules (${\rm C_{2}H_{6}O}$) at
high external magnetic field. Although ethanol typically exists as a liquid,
we employ its solid configuration as an example of an ordered sample with
strong homonuclear dipole-dipole couplings. In particular, ethanol molecules
exhibit dipolar couplings of up to 17 kHz (the proton attached to the oxygen
shows limited dipole interaction with the rest of the system so we exclude it
from the simulations). High external fields improve nuclear magnetic resonance
procedures, not only because it yields higher polarization rates, but also
because it enhances the weaker, and thus harder to detect, energy shifts. Here
we consider $B_{0}=2.1$ T and chemical shifts of 3.66 ppm and 1.19 ppm,
resulting in shifts of approximately 327 Hz and 106 Hz, respectively.

Our numerical simulation unfolds in two phases. First we find the target
magnetic signal by simulating the evolution of the nuclear spin sample
subjected to the LG4 decoupling sequence. The approximate Hamiltonian in Eq.
(1) facilitates a deeper understanding of the nuclear dynamics and in
particular the development of the geometrical interpretation that has set the
ground for the design of our protocol. Our simulations, however, make use of
the exact nuclear spin Hamiltonian, which reads

$\displaystyle H(t)$
$\displaystyle=\sum_{i=1}^{N=5}\left\\{-\gamma_{h}\delta_{i}B_{0}I_{z}^{i}+\left[\Omega+\eta(t)\right]I_{\phi}^{i}+\Delta
I_{z}^{i}\right\\}+$ (10)
$\displaystyle+\sum_{i>{j=1}}^{N=5}-\frac{\mu_{0}\hbar\gamma_{n}^{2}}{8\pi|r^{ij}|^{3}}\left(3r^{ij}_{z}-1\right)\left[3I_{z}^{i}I_{z}^{j}-\vec{I}_{i}\cdot\vec{I}_{j}\right],$

where $\delta_{i}$ is the target nuclear shift of the $i$th hydrogen atom and
$\eta(t)$ is the driving noise modeled with an Ornstein-Uhlenbeck process with
a $1$ ms correlation time and 0.24% amplitude.

We assume the sample starting in a completely mixed state. A triggering RF
pulse sets the desired initial state $\rho(0)$, a thermal state oriented along
the axis perpendicular to $A$ and $B$. From there, the evolution of the
nuclear density matrix is simulated using a master equation that includes
$T_{2}^{*}=0.2$ s relaxation,

$\dot{\rho}=-i\left[H,\rho\right]+\frac{1}{2T^{*}_{2}}\sum_{j=1}^{N=5}\left(4{I}^{j}_{z}\rho{I}^{j}_{z}-\rho\right),$
(11)

leading to a signal computed as

$s(t)=\frac{\gamma_{h}\hbar\mu_{0}\sigma_{h}g}{4\pi}\operatorname{Tr}\left[\rho(t)\bar{I_{z}}\right],$
(12)

where $\sigma_{h}=5.2\times 10^{28}\mathrm{m^{-3}}$ is the number density of
hydrogen spins for ethanol, and $g\approx~{}4.1$ is a geometric factor that
relates the sample magnetization and the magnetic field in the NV location,
see Glenn18 ; Munuera23  for further details.

In the second phase, we simulate the evolution of the NV ensemble interacting
with $s(t)$ and subjected to the sensing MW pulse sequence of our protocol.
The Hamiltonian that governs the dynamics of each NV centers reads

$H=\gamma_{e}s(t)\frac{\sigma_{z}}{2}+C(t)\frac{\sigma_{z}}{2}+\frac{\Omega_{\rm
NV}(t)\sigma_{\phi}}{2},$ (13)

with $\Omega_{\text{NV}}(t)$ the control Rabi frequency, and
$C(t)\frac{\sigma_{z}}{2}$ describing potential RF-induced crosstalk on the
NVs. Following the protocol devised in this work, they interact with the
signals produced by the nuclear spin rotations around axis $A$, $\bar{A}$ and
$\bar{B}$ and accumulate a phase determined by the state of the sample
magnetization. During the time that corresponds to the delivery of the RF
field over the sample, we tranform the accumulated phase into a population
difference with a $\pi/2$ pulse and simulate the measurement, after which the
sensor is reinitilized and we simulate the detection of the signal produced by
the next LG4 block. Finally, a Fourier transform of the measurements provides
the spectra displayed in Fig. (III), which proves the ability of our protocol
to access the chemical shifts of the molecule.

Figure (III) shows three different experiments with increasing RF intensities.
As expected, stronger RF drivings lead to clearer spectra, less distorted by
spurious peaks. In particular we simulate RF drivings with Rabi frequencies of
$(2\pi)\times$100 kHz, $(2\pi)\times$150 kHz, and $(2\pi)\times$200 kHz, all
attainable values by state of the art antennas Herb20 ; Yudilevich23 , and set
the Rabi frequency of the MW control at 20 MHz in all cases. As intended, our
method leads to resonance peaks centred in $\delta_{i}^{*}$ from which one can
extract the target nuclear shifts $\delta_{i}$ using Eq. (5). For comparison,
we include the resutls of a fourth simulation using AERIS Munuera23 , which
does not incorporate any dipolar coupling suppression technique. In this case,
the obtained spectra (black-curve) is distorted as a consequence of the strong
nuclear dipolar couplings.

In summary, we have demonstrated that our protocol effectively identifies the
target energy shifts $\delta_{i}$ with strong nuclear dipole-dipole
interactions at high external magnetic fields.

##  IV Conclusions

We have designed a protocol that utilizes LG4 sequences and a tailored NV
pulse train to identify chemical shifts in the presence of strong dipole-
dipole interactions. The RF field serves two key purposes: (i) decoupling
nuclear spins and (ii) generating a nuclear signal oscillating at a moderate
frequency that can be measured by the NVs, allowing the protocol to operate at
high magnetic fields. By incorporating a tailored MW sequence on the NV for
signal detection, we achieve effective retrieval of chemical shifts. Finally,
the accuracy of our method is ultimately limited by the nuclear sample
decoherence, thus surpassing the limitations imposed by NVs dephasing and
thermalization. Our findings pave the way for the advancement of microscale
NMR techniques and broaden their application in diverse fields, such as
materials science, chemistry, and biology.

##  V Acknowledgements

C.M.-J. acknowledges the predoctoral MICINN grant PRE2019-088519. J. C.
acknowledges the Ramón y Cajal (RYC2018-025197-I) research fellowship. Authors
acknowledge the Quench project that has received funding from the European
Union’s Horizon Europe – The EU Research and Innovation Programme under grant
agreement No 101135742, the Spanish Government via the Nanoscale NMR and
complex systems project PID2021-126694NB-C21, and the Basque Government grant
IT1470-22. A.T. acknowledges support from the Horizon Europe project QCircle
101059999 (Teaming for Excellence).

## References

  * (1) J. P. Dowling, and G. J. Milburn, Quantum technology: the second quantum revolution, Phil. Trans. R. Soc. A. 361, 1655 (2003).
  * (2) C. L. Degen, F. Reinhard, and P. Cappellaro, Quantum sensing, Rev. Mod. Phys. 89, 035002 (2017).
  * (3) M. H. Levitt, Spin Dynamics: Basics of Nuclear Magnetic Resonance, 2nd ed. (Wiley, West Sussex, 2008).
  * (4) M. W. Doherty, N. B. Manson, P. Delaney, F. Jelezko, J. Wrachtrup, and L. C. L. Hollenberg, The nitrogen-vacancy colour centre in diamond, Phys. Rep. 528, 1 (2013).
  * (5) J. M. Boss, K. S. Cujia, J. Zopes, and C. L. Degen, Quantum sensing with arbitrary frequency resolution, Science 356, 837 (2017).
  * (6) S. Schmitt, T. Gefen, F. M. Stürner, T. Unden, G. Wolff, C. Müller, J. Scheuer, B. Naydenov, M. Markham, S. Pezzagna, J. Meijer, I. Schwarz, M. B. Plenio, A. Retzker, L. P. McGuinness, and F. Jelezko, Submillihertz magnetic spectroscopy performed with a nanoscale quantum sensor, Science 356, 832 (2017).
  * (7) D. R. Glenn, D. B. Bucher, J. Lee, M. D. Lukin, H. Park, and R. L. Walsworth, High-resolution magnetic resonance spectroscopy using a solid-state spin sensor, Nature 555, 351 (2018).
  * (8) N. Arunkumar, D. B. Bucher, M. J. Turner, P. TomHon, D. Glenn, S. Lehmkuhl, M. D. Lukin, H. Park, M. S. Rosen, T. Theis, and R. L. Walsworth, Micron-Scale NV-NMR Spectroscopy with Signal Amplification by Reversible Exchange, PRX Quantum 2, 010305 (2021).
  * (9) D. B. Bucher, D. R. Glenn, H. Park, M. D. Lukin, and R. L. Walsworth, Hyperpolarization-Enhanced NMR Spectroscopy with Femtomole Sensitivity Using Quantum Defects in Diamond, Phys. Rev. X 10, 021053 (2020).
  * (10) K. Uǧurbil, G. Adriany, P. Andersen, W. Chen, M. Garwood, R. Gruetter, P. G. Henry, S. G. Kim, H. Lieu, I. Tkac, T. Vaughan, P. F. Van De Moortele, E. Yacoub, and X. H. Zhu, Ultrahigh field magnetic resonance imaging and spectroscopy, Magn. Reson. Imaging 21, 1263 (2003).
  * (11) P. Alsina-Bolívar, A. Biteri-Uribarren, C. Munuera-Javaloy, and J. Casanova, J-coupling NMR Spectroscopy with Nitrogen Vacancy Centers at High Fields, arXiv preprint:2311.11880 (2023).
  * (12) C. Munuera-Javaloy, A. Tobalina, and J. Casanova, High-Resolution NMR Spectroscopy at Large Fields with Nitrogen Vacancy Centers, Phys. Rev. Lett. 130, 133603 (2023).
  * (13) J. Meinel, M. Kwon, R. Maier, D. Dasari, H. Sumiya, S. Onoda, J. Isoya, V. Vorobyov, and J. Wrachtrup, High-resolution nanoscale NMR for arbitrary magnetic fields, Commun. Phys. 6, 302 (2023).
  * (14) D. Daly, S.J. DeVience, E. Huckestein, J.W. Blanchard, J. Cremer and R.L. Walsworth, Nutation-Based Longitudinal Sensing Protocols for High-Field NMR With Nitrogen-Vacancy Centers in Diamond,  arXiv preprint:2310.08499 (2023).
  * (15) K. R. Mote, V. Agarwal, and P. K. Madhu, Five decades of homonuclear dipolar decoupling in solid-state NMR: Status and outlook, Prog. Nucl. Magn. Reson. Spectrosc. 97, 1 (2016).
  * (16) D. M. Pisklak, M. Zielińska-Pisklak, L. Szeleszczuk, I. Wawer, 13C cross-polarization magic-angle spinning nuclear magnetic resonance analysis of the solid drug forms with low concentration of an active ingredient-propranolol case, J. Pharm. Biomed. Anal. 93, 68 (2014).
  * (17) D. M. Pisklak, M. A. Zielińska- Pisklak, L. Szeleszczuk, I. Wawer, 13C solid-state NMR analysis of the most common pharmaceutical excipients used in solid drug formulations, Part I: Chemical shifts assignment, J. Pharm. Biomed. Anal. 122, 81 (2016).
  * (18) H. Nie, Y. Su, M. Zhang, Y. Song, A. Leone, L. S. Taylor, P. J. Marsac, T. Li, and S. R. Byrn, Solid-State Spectroscopic Investigation of Molecular Interactions between Clofazimine and Hypromellose Phthalate in Amorphous Solid Dispersions, Mol. Pharmaceutics, 13 3964-3975 (2016).
  * (19) A. Marchetti, J. Yin, Y. Su, X. Kong, Solid-state NMR in the field of drug delivery: State of the art and new perspectives, MRL 1, 28-70 (2021).
  * (20) R. Tycko, Solid State NMR Studies of Amyloid Fibril Structure, Annu. Rev. Phys. Chem. 62, 279-299 (2011).
  * (21) O. Pecher, J. Carretero-González, K. J. Griffith, and C. P. Grey, Materials’ Methods: NMR in Battery Research, Chem. Mater. 29, 213-242 (2017).
  * (22) K. Herb, J. Zopes, K. S. Cujia, and C. L. Degen, Broadband radio-frequency transmitter for fast nuclear spin control,  Rev. Sci. Instrum. 91, 113106 (2020).
  * (23) D. Yudilevich, A. Salhov, I. Schaefer, K. Herb, A. Retzker, and A. Finkler, Coherent Manipulation of nuclear spins in the strong driving regime,  New. J. Phys. 25, 113042 (2023.
  * (24) M. Lee, and W. I. Goldburg, Nuclear-Magnetic-Resonance Line Narrowing by a Rotating rf Field, Phys. Rev. 140, 1261 (1965).
  * (25) M. Mehring, and J. S. Waught, Magic-Angle NMR Experiments in Solids, Phys. Rev. B 5, 3459 (1972).
  * (26) E. Vinogradov, P.K. Madhu, S. Vega, High-resolution proton solid-state NMR spectroscopy by phase-modulated Lee-Goldburg experiment, Chem. Phys. Lett. 314 443 (1999).
  * (27) M. E. Halse, and L. Emsley, Improved Phase-Modulated Homonuclear Dipolar Decoupling for Solid-State NMR Spectroscopy from Symmetry Considerations, J. Phys. Chem. A 117, 5280 (2013).
  * (28) H. Y. Carr, and E. M. Purcell, Effects of Diffusion on Free Precession in Nuclear Magnetic Resonance Experiments, Phys. Rev. 94, 630 (1954).
  * (29) S. Meiboom, and D. Gill, Modified Spin-Echo Method for Measuring Nuclear Relaxation Times, Rev. Sci. Instrum. 29, 688-691 (1958).

##  Appendix A Nuclear spin dynamics under RF drivings

Under an RF field (that will rotate nuclei around the $A,\bar{A},B,$ or
$\bar{B}$ axes) the nuclear spin Hamiltonian including dipole-dipole terms
among nuclear spins reads

$\displaystyle
H=\sum_{i}\left[\gamma_{n}B_{z}I^{i}_{z}+\delta_{j}I^{i}_{z}+2\Omega
I^{i}_{x}\sin{\left(\omega_{d}t-\alpha\right)}\right]+\sum_{i>j}\frac{\mu_{0}\gamma^{2}_{n}\hbar}{4\pi
r_{i,j}^{3}}\bigg{[}\vec{I}_{i}\cdot\vec{I}_{j}-3(\vec{I}_{i}\cdot\hat{r}_{i,j})(\vec{I}_{j}\cdot\hat{r}_{i,j})\bigg{]},$
(14)

where $r_{i,j}$ is the distance between each pair of nuclei ($\hat{r}_{i,j}$
its a unitary vector such that $\vec{r}_{i,j}=r_{i,j}\hat{r}_{i,j}$),
$\gamma_{N}$ is the nuclear gyromagnetic ratio, $\mu_{0}$ is the vacuum
permeability, $\vec{I}_{i}={\left(I^{i}_{x},I^{i}_{y},I^{i}_{z}\right)}$ are
the nuclear spin operators for the $i$th spin, $\Omega$ and $\omega_{d}$ are
the Rabi and carrier frequencies of the radio-frequency (RF), $\alpha$ is a
tunable phase of the RF, and $\delta_{i}$ represents the deviation (i.e. the
energy shift) of the $i$th nuclear spin from the Larmor precession rate
$\omega_{L}=\gamma_{n}B_{z}$ owing to its particular magnetic environment. The
accurate determination of $\delta_{j}$ is the target of the sensing protocol
introduced here.

In a rotating frame w.r.t. $(\omega_{L}-\Delta)\sum_{i}I_{z}^{i}$, and under
the secular approximation of the dipole-dipole term that eliminates fast
rotating terms by invoking the rotating wave approximation, Eq. (14)
simplifies to

$\displaystyle H=\sum_{i}\left[(\Delta+\delta_{i})I_{z}^{i}+\Omega
I^{i}_{\alpha}\right]+\sum_{i>j}\frac{\mu_{0}\gamma^{2}_{n}\hbar}{4\pi
r_{i,j}^{3}}\left[1-3\left(r_{z}^{i,j}\right)^{2}\right]\left[I^{i}_{z}I^{j}_{z}-\frac{1}{2}(I^{i}_{\alpha}I^{j}_{\alpha}+I^{i}_{\alpha^{\perp}}I^{j}_{\alpha^{\perp}})\right].$
(15)

where $I^{i}_{\alpha}=\left(I^{i}_{x}\sin\alpha+I^{i}_{y}\cos\alpha\right)$,
and
${I^{i}_{\alpha}}^{\perp}=\left(I^{i}_{x}\cos\alpha-I^{i}_{y}\sin\alpha\right)$.

Introducing a new spin basis, defined by rotating the original axes around
$\alpha^{\perp}$,

$\displaystyle
I_{P}^{j}=\cos{(\theta)}I_{z}^{j}+\sin{(\theta)}I_{\alpha}^{j},$
$\displaystyle
I_{Q}^{j}=\cos{(\theta)}I_{\alpha}^{j}-\sin{(\theta)}I_{z}^{j},$
$\displaystyle I_{Q^{\perp}}^{j}=I_{\alpha^{\perp}}^{j},$ (16)

and defining the rotation angle through
$\cos{\theta}=\frac{\Delta}{\sqrt{\Omega^{2}+\Delta^{2}}}$, and
$\sin{\theta}=\frac{\Omega}{\sqrt{\Omega^{2}+\Delta^{2}}}$, allows to rewrite
the sample Hamiltonian as

$\displaystyle
H=\bar{\Omega}\sum_{i}I_{P}^{i}+\sum_{i}\delta_{i}[\cos{(\theta)}I_{P}^{i}-\sin{(\theta)}I_{Q}^{i}]+\sum_{i>j}\frac{\mu_{0}\gamma^{2}_{n}\hbar}{4\pi
r_{i,j}^{3}}\left[1-3(r_{i,j}^{z})^{2}\right]\Bigg{\\{}\cos^{2}{(\theta)}I_{P}^{i}I_{P}^{j}+\sin^{2}{(\theta)}I_{Q}^{i}I_{Q}^{j}$
(17)
$\displaystyle-\cos(\theta)\sin(\theta)(I_{P}^{i}I_{Q}^{j}+I_{Q}^{i}I_{P}^{j})-\frac{1}{2}\bigg{[}\cos^{2}{(\theta)}I_{Q}^{i}I_{Q}^{j}+\sin^{2}{(\theta)}I_{P}^{i}I_{P}^{j}+\cos(\theta)\sin(\theta)(I_{P}^{i}I_{Q}^{j}+I_{Q}^{i}I_{P}^{j})+I_{Q^{\perp}}^{i}I_{Q^{\perp}}^{j}\bigg{]}\Bigg{\\}},$

where the effective rotation rate around $I_{P}$ reads
$\bar{\Omega}=\sqrt{\Delta^{2}+\Omega^{2}}$. Finally, many terms can be
neglected by a secular approximation with respect to
$\bar{\Omega}\sum_{i}I_{P}^{i}$. The remaining terms in the dipolar
interaction disappear magically when the angle that defines the change of
basis in Eq. (A) satisfies $\cos(\theta)=\pm 1/\sqrt{3}$, or, equivalently,
when the Lee-Goldburg condition $\Delta=\pm\Omega/\sqrt{2}$ is met, leading to

$H=\sum_{i=1}^{N}\left(\frac{\pm\delta_{i}}{\sqrt{3}}+\bar{\Omega}\right)I^{i}_{P},$
(18)

where $\pm\delta_{j}/\sqrt{3}$ are the parallel components of the shifts with
respect to the effective rotation axis P, and its sign is the same as the sign
of $\Delta$. Note that any combination of $\Omega$ and $\Delta$ that complies
with the Lee-Goldburg condition produces the described decoupling effect. In
particular, for a given intensity of the RF field, this can be detuned from
the top and from the bottom with respect to the Larmor. Moreover, the previous
derivation is valid for any phase $\alpha$ of the RF field. This freedom has
been exploited to develop more elaborated control schemes that concatenate
various RF fields, such as the LG4 sequence implemented in our protocol.

In the LG4 sequence, each driving axis is applied during a time
$T=2\pi/{\bar{\Omega}}$ following the order $A$, $\bar{A}$, $\bar{B}$, and $B$
(see main text). In order to obtain the effective dynamics of a full LG4
block, we write the explicit propagator

$U_{\rm
LG4}=U_{B}U_{\bar{B}}U_{\bar{A}}U_{A}=e^{-i\sum_{i=1}^{N}\left(\frac{\delta_{i}}{\sqrt{3}}+\bar{\Omega}\right)I^{i}_{B}T}e^{-i\sum_{i=1}^{N}\left(-\frac{\delta_{i}}{\sqrt{3}}+\bar{\Omega}\right)I^{i}_{\bar{B}}T}e^{-i\sum_{i=1}^{N}\left(-\frac{\delta_{i}}{\sqrt{3}}+\bar{\Omega}\right)I^{i}_{\bar{A}}T}e^{-i\sum_{i=1}^{N}\left(\frac{\delta_{i}}{\sqrt{3}}+\bar{\Omega}\right)I^{i}_{A}T}.$
(19)

In every propagator, we can do the following change

$e^{-i\sum_{i=1}^{N}\left(\pm\frac{\delta_{i}}{\sqrt{3}}+\bar{\Omega}\right)I^{i}_{P}T}=e^{-i\sum_{i=1}^{N}\pm\frac{\delta_{i}}{\sqrt{3}}I^{i}_{P}T}e^{-i\sum_{i=1}^{N}\bar{\Omega}I^{i}_{P}T}=e^{-i\sum_{i=1}^{N}\pm\frac{\delta_{i}}{\sqrt{3}}I^{i}_{P}T},$
(20)

where we used that
$e^{-i\sum_{i=1}^{N}\bar{\Omega}I^{i}_{P}T}=e^{-i\sum_{i=1}^{N}2\pi
I^{i}_{P}}=\mathbb{I}$. Assuming that
$\bar{\Omega}>>\pm\frac{\delta_{i}}{\sqrt{3}}$, we can Trotterize the LG4
propagator to obtain

$e^{-i\sum_{i=1}^{N}\left(\frac{\delta_{i}}{\sqrt{3}}I^{i}_{B}-\frac{\delta_{i}}{\sqrt{3}}I^{i}_{\bar{B}}-\frac{\delta_{i}}{\sqrt{3}}I^{i}_{\bar{A}}+\frac{\delta_{i}}{\sqrt{3}}I^{i}_{A}\right)T}.$
(21)

Finally, substituting the expression for each axis operator of Eq. (II.1),
obtain the propagator

$e^{-i\sum_{i=1}^{N}\left[\frac{\delta_{i}}{\sqrt{3}\bar{\Omega}}\left(\Omega
I^{i}_{y}\cos\alpha+\Delta I^{i}_{z}\right)\right]4T}.$ (22)

From this expression, we reach the final effective Hamiltonian (4) after
rearranging the terms

$H_{\rm eff}=\sum_{i}\delta^{*}_{i}I^{i}_{C},$ (23)

where
$I^{i}_{C}=\frac{\sqrt{2}I^{i}_{y}\cos{\alpha}+I^{i}_{z}}{\sqrt{2\cos^{2}{\alpha}+1}}$
and $\delta_{i}^{*}=\delta_{i}\frac{\sqrt{1+2\cos^{2}{\alpha}}}{3}$.

##  Appendix B Accumulated Phase

As stated in the main text, the signals received by the NV adhere to a general
form Eq.(3). When a two pulse CPMG sequence is applied on the NV sensor (see
Fig.(1)) with $\pi$ pulses applied at times $t_{1}$ and $t_{2}$, the phase
accumulated by the NV at stage $k$ is:

$\Phi_{k}=\int_{0}^{t_{1}}\left[|\gamma_{e}|\Gamma_{k}\cos{\left(\bar{\Omega}t+\phi_{k}\right)}+b_{k}\right]dt-\int_{t_{1}}^{t_{2}}\left[|\gamma_{e}|\Gamma_{k}\cos{\left(\bar{\Omega}t+\phi_{k}\right)}+b_{k}\right]dt+\int_{t_{2}}^{T}\left[|\gamma_{e}|\Gamma_{k}\cos{\left(\bar{\Omega}t+\phi_{k}\right)}+b_{k}\right]dt,$
(24)

where we choose the separation of both pulses to be $\frac{T}{2}$, which
ensures the cancellation of the static $b_{0}$ term

$\Phi_{k}=\frac{2|\gamma_{e}|\Gamma_{k}}{\bar{\Omega}}\left[\sin{(\bar{\Omega}t_{1}+\phi_{k})}-\sin{(\bar{\Omega}t_{2}+\phi_{k})}\right]=\frac{4|\gamma_{e}|\Gamma_{k}}{\bar{\Omega}}\cos{\left(\phi_{k}-\varphi\right)},$
(25)

with $\varphi=\frac{\pi}{2}-\bar{\Omega}t_{1}$.

As the sample evolves under the LG4 sequence, the amplitude $\Gamma_{k}$ and
phase $\phi_{k}$ of the NMR signal evolve, see Fig. (2) (a, b). If the signal
gets projected about some axis, e.g. $\Gamma_{k}\cos{\phi_{k}}$, the variation
of this projection is a simple sinusoidal function (see Fig. (2) (c)) which is
exactly what we need in order to extract the information using a discrete
Fourier transform. This result can be understood geometrically, see main text.

Once we choose a projection angle axis, we can compute the adequate timing for
the CPMG sequence as

$\varphi=\varphi_{\rm opt}\rightarrow\varphi_{\rm
opt}=\frac{\pi}{2}-\bar{\Omega}t_{1}\rightarrow
t_{1}=\frac{\pi}{2\bar{\Omega}}-\frac{\varphi_{\rm opt}}{\bar{\Omega}}.$ (26)

For optimal pulse positions, we select the angle matching the major axis of
the ellipse. This axis is orthogonal to both $\hat{A}$ and $\hat{C}$, i.e.,
$\left(0,-\frac{1}{\sqrt{2+\cos{2\alpha}}},\frac{\sqrt{2}\cos{\alpha}}{\sqrt{2+\cos{2\alpha}}}\right)$.
Then, the angle $\theta_{A}$ is measured with respect to the orthogonal
component of $\hat{z}$ concerning $\hat{A}$. This angle is:

$\varphi_{\rm
opt}=\arccos{\frac{\sqrt{3}\cos{\alpha}}{\sqrt{2+\cos{2\alpha}}}}.$ (27)

##  Appendix C Analytical expression

Here we provide details of the derivation of the analytical expression for the
expected value of the measurements performed with the NV. Our starting point
is the fact that the NV will couple to a signal proportional to the $\hat{z}$
component of the sample magnetization.

Focusing on the $k$th driving stage around $\hat{A}$, we can describe the
expected signal as:

$s\propto\hat{M}(t)\cdot\hat{z}=\hat{M}(t)\left(\hat{z}^{\perp}\sin{\theta_{\rm
LG}}+\hat{A}\cos{\theta_{\rm LG}}\right),$ (28)

where $\hat{M}(t)$ is the magnetization vector and the $\hat{z}$ axis was
split in the parallel and perpendicular components with respect to axis
$\hat{A}$, and $\theta_{\rm LG}=\arccos{\frac{1}{\sqrt{3}}}$ is the magic
angle. We can describe the time dependency of the magnetization during the
driving stage $A$ by employing the Rodrigues’ rotation formula as

$\hat{M}(t)=\hat{M}_{k}\cos{\bar{\Omega}t}+\left(\hat{A}\times\hat{M}_{k}\right)\sin{\bar{\Omega}t}+\hat{A}\left(\hat{A}\cdot\hat{M}_{k}\right)\left(1-\cos{\bar{\Omega}t}\right),$
(29)

where $\hat{M}_{k}$ is the magnetization vector at the beginning of the $k$th
sequence. Substituting in Eq. (28), we get

$s\propto\left[\hat{M}_{k}\cdot\hat{z}^{\perp}\cos{\bar{\Omega}t}+\left(\hat{A}\times\hat{M}_{k}\right)\cdot\hat{z}^{\perp}\sin{\bar{\Omega}t}\right]\sin{\theta_{\rm
LG}}+\hat{A}\cdot\hat{M}_{k}\cos{\theta_{\rm LG}}.$ (30)

We can now split the magnetization vector into its parallel and perpendicular
components with respect to $\hat{A}$ as
$\hat{M}_{k}=\left(\vec{M}_{k}^{\parallel}+\vec{M}_{k}^{\perp}\right)$. With
this we reach expression

$s\propto|\vec{M}_{k}^{\perp}|\sin{\theta_{\rm
LG}}\cos{\left(\bar{\Omega}t+\phi\right)}+|\vec{M}_{k}^{\parallel}|\cos{\theta_{\rm
LG}},$ (31)

where $\phi$ is the angle between $\vec{M}_{k}^{\perp}$ and $\hat{z}^{\perp}$.
Notice how this expression exactly matches the shape of Eq.(3) in the main
text.

Substituting in Eq. (8), we obtain

$\Phi\propto-\frac{4\gamma_{e}\sin{\theta_{\rm
LG}}}{\bar{\Omega}}|\vec{M}_{k}^{\perp}|\cos{\left(\phi-\varphi\right)}=-\frac{4\gamma_{e}\sin{\theta_{\rm
LG}}}{\bar{\Omega}}\hat{M}_{k}\cdot\hat{l}$ (32)

with $\hat{l}$ a vector perpendicular to $\hat{A}$ and tilted $\varphi$ with
respect to $\hat{z}^{\perp}$.

We can now generalize to all the driving stages by describing the precession
motion of the initial magnetization vectors employing Rodrigues’ formula once
again

$\hat{M}_{k}=\hat{M}_{0}\cos{\left(\frac{4\delta_{i}^{*}k}{\bar{\Omega}}\right)}+\left(\hat{C}\times\hat{M}_{0}\right)\sin{\left(\frac{4\delta_{i}^{*}k}{\bar{\Omega}}\right)}+\hat{C}\left(\hat{C}\cdot\hat{M}_{0}\right)\left[1-\cos{\left(\frac{4\delta_{i}^{*}k}{\bar{\Omega}}\right)}\right].$
(33)

Starting with an initial magnetization $\hat{M}_{0}$ in the orthogonal plane
with respect to $\hat{C}$ and an angle $\mu$ with respect to $\hat{x}$ (which
resides in this plane), and including factors for the signal amplitude, we
obtain the formula for the accumulated phase

$\Phi_{k}=D_{\varphi}\rho_{i}\cos{\left(\frac{4\delta_{i}^{*}k}{\bar{\Omega}}+\mu-\beta_{\varphi}\right)},$
(34)

where
$D_{\varphi}=\frac{-\gamma_{e}\hbar^{2}\gamma_{h}^{2}\mu_{0}g\sin{\left(\theta_{\rm
LG}\right)}}{8\bar{\Omega}\pi^{2}k_{B}T}\sqrt{\left(\frac{\cos{\varphi}\sin{\alpha}}{\sqrt{3}}-\cos{\alpha}\sin{\varphi}\right)^{2}+\frac{\left(\sqrt{3}\cos{\alpha}\cos{\varphi}+\sin{\alpha}\sin{\varphi}\right)^{2}}{2+\cos{\left(2\alpha\right)}}}$,
$\rho_{i}$ is the spin density of the $i$th nucleus, and
$\beta_{\varphi}=\arctan{\frac{3\left(\sqrt{3}\cos{\alpha}\cos{\varphi}+\sin{\alpha}\sin{\varphi}\right)}{\sqrt{2+\cos{(2\alpha)}}\left(\sqrt{3}\cos{\varphi}\sin{\alpha}-3\cos{\alpha}\sin{\varphi}\right)}}$.
Here, $g$ is a geometric factor that relates the sample geometry with the
signal amplitude in the NV site, $k_{B}$ is the Boltzmann constant, and $T$ is
the temperature. See Glenn18 ; Munuera23  for further details on the signal
amplitude expression. It can be checked that $\varphi_{\rm opt}$ does indeed
maximize $D_{\varphi}$. The total accumulated phase of the three drivings $A$,
$\bar{A}$, $B$ is simply $3\Phi_{k}$, provided that
$\nu_{\varphi}=\mu-\beta_{\varphi}$ is the same in the three stages, which in
our case we choose to add up to $0$.

Finally, to consider all effective chemical shifts $\delta^{*}_{i}$ it
suffices to sum all the contributions. Assuming a small angle $\Phi_{k}$, the
final formula for the expected value of $\sigma_{z}$ is

$\langle\sigma_{z}\rangle_{k}\approx
3D_{\varphi}\sum_{i}{\left[\rho_{i}\cos{\left(\frac{4\delta_{i}^{*}k}{\bar{\Omega}}+\nu_{\varphi}\right)}\right]},$
(35)

which gives us the desired spectrum upon Fourier transform.