Skip to main content
Proof Assistants Beta
march's user avatar
march's user avatar
march's user avatar
march
  • Member for 2 years, 4 months
  • Last seen more than a month ago
  • Washington State, USA
Profile Activity
Stats
373
reputation
1k
reached
0
answers
3
questions
Communities
View all
About

Theoretical physics: theory of Bose-Einstein condensates of polar molecules, plasmonics.

Mathematics: dabbler.

Badges
View all badges
This user doesn’t have any gold badges yet.
4
silver badges
10
bronze badges
Top tags
0
Score
3
Posts
100
Posts %
0
Score
2
Posts
67
Posts %
0
Score
1
Posts
33
Posts %
0
Score
1
Posts
33
Posts %
0
Score
1
Posts
33
Posts %
0
Score
1
Posts
33
Posts %
Top posts
12
In Lean, why is the exact tactic necessary when the goal is the same as a hypothesis?
Feb 10, 2022
9
Has there been any work on automated translation of tactic proofs to everyday language?
Feb 12, 2022
6
How do we resolve metavariables that appear in hypotheses and targets in Lean?
Feb 18, 2022
Top Meta posts
1
1
11
Should there be a mathlib tag for Lean?
Top network posts
View all network posts
42
Why do we hear frequencies in the basis of sine waves?
28
Is there a quasistatic process that is not reversible?
26
Is there a GraphicsPrimitiveQ (or a complete list of Heads of graphics primitives)?
25
Why doesn't PlusMinus[a]^2 simplify to a^2?
23
What has changed in pattern matching functions with the Orderless attribute?